theorem not_symm_not {α : Type u_1} {a b : α} {r : α → α → Prop} [Std.Symm r] : ¬r a b → ¬r b a

theorem not_comm_not {α : Type u_1} {a b : α} {r : α → α → Prop} [Std.Symm r] : ¬r a b ↔ ¬r b a

theorem trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {a : α} {x : β} {u : γ} {r : α → β → Prop} {s : β → γ → Prop} {t : α → γ → Prop} [Trans r s t] (hr : r a x) (hs : s x u) : t a u

def Relation.«term_ᵀ» : Lean.TrailingParserDescr

Relation

Heterogeneous relations

converse is flip

Equations

• Relation.«term_ᵀ» = Lean.ParserDescr.trailingNode `Relation.«term_ᵀ» 1050 0 (Lean.ParserDescr.symbol "ᵀ")

@[simp]

theorem Relation.compl_apply {α : Type u_1} {β : Type u_2} {a : α} {x : β} {r : α → β → Prop} : (r a x)ᶜ ↔ ¬r a x

@[simp]

theorem Relation.flip_apply {α : Type u_1} {a b : α} (r : α → α → Prop) : flip r a b ↔ r b a

def Relation.domain {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : Set α

Equations

• Relation.domain r = {x : α | ∃ (y : β), r x y}

def Relation.codomain {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : Set β

Equations

• Relation.codomain r = {y : β | ∃ (x : α), r x y}

@[simp]

theorem Relation.mem_domain_iff {α : Type u_1} {β : Type u_2} {a : α} (r : α → β → Prop) : a ∈ domain r ↔ ∃ (x : β), r a x

@[simp]

theorem Relation.mem_codomain_iff {α : Type u_1} {β : Type u_2} {x : β} (r : α → β → Prop) : x ∈ codomain r ↔ ∃ (a : α), r a x

theorem Relation.left_mem_domain {α : Type u_1} {β : Type u_2} {a : α} {x : β} {r : α → β → Prop} (hr : r a x) : a ∈ domain r

theorem Relation.right_mem_codomain {α : Type u_1} {β : Type u_2} {a : α} {x : β} {r : α → β → Prop} (hr : r a x) : x ∈ codomain r

@[simp]

theorem Relation.domain_flip {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : domain (flip r) = codomain r

@[simp]

theorem Relation.codomain_flip {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : codomain (flip r) = domain r

theorem Relation.domain_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : α → β → Prop) (s : β → γ → Prop) : domain (Comp r s) ⊆ domain r

theorem Relation.codomain_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : α → β → Prop) (s : β → γ → Prop) : codomain (Comp r s) ⊆ codomain s

theorem Relation.domain_mono {α : Type u_1} {β : Type u_2} {r r' : α → β → Prop} (h : r ≤ r') : domain r ⊆ domain r'

theorem Relation.codomain_mono {α : Type u_1} {β : Type u_2} {r r' : α → β → Prop} (h : r ≤ r') : codomain r ⊆ codomain r'

def Relation.Domp {α : Type u_1} {β : Type u_2} (r s : α → β → Prop) : α → β → Prop

Double composition of r of the converse of s

Equations

• Relation.Domp r s = Relation.Comp r (Relation.Comp (flip s) r)

theorem Relation.domp_def {α : Type u_1} {β : Type u_2} (r s : α → β → Prop) : Domp r s = Comp (Comp r (flip s)) r

theorem Relation.domp_def' {α : Type u_1} {β : Type u_2} (r s : α → β → Prop) : Domp r s = Comp r (Comp (flip s) r)

theorem Relation.domain_domp {α : Type u_1} {β : Type u_2} (r s : α → β → Prop) : domain (Domp r s) ⊆ domain r

theorem Relation.codomain_domp {α : Type u_1} {β : Type u_2} (r s : α → β → Prop) : codomain (Domp r s) ⊆ codomain r

theorem Relation.le_domp_self {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : r ≤ Domp r r

theorem Relation.domp_mono {α : Type u_1} {β : Type u_2} {r₁ r₂ s₁ s₂ : α → β → Prop} (hr : r₁ ≤ r₂) (hs : s₁ ≤ s₂) : Domp r₁ s₁ ≤ Domp r₂ s₂

@[simp]

theorem Relation.domp_bot_right {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : Domp r ⊥ = ⊥

@[simp]

theorem Relation.domp_bot_left {α : Type u_1} {β : Type u_2} (s : α → β → Prop) : Domp ⊥ s = ⊥

theorem Relation.domp_sup_right {α : Type u_1} {β : Type u_2} (r s₁ s₂ : α → β → Prop) : Domp r (s₁ ⊔ s₂) = Domp r s₁ ⊔ Domp r s₂

theorem Relation.domp_or {α : Type u_1} {β : Type u_2} (r s t : α → β → Prop) : (Domp r fun (x : α) (y : β) => s x y ∨ t x y) = fun (x : α) (y : β) => Domp r s x y ∨ Domp r t x y

class Relation.Dompeq {α : Type u_1} {β : Type u_2} (r s : α → β → Prop) : Prop

• dompeq : Domp r s = s

theorem Relation.domp_eq {α : Type u_1} {β : Type u_2} (r s : α → β → Prop) [Dompeq r s] : Domp r s = s

@[instance_reducible]

instance Relation.instTransCompFlipOfDompeq {α : Type u_1} {β : Type u_2} {r r' : α → β → Prop} [Dompeq r r'] : Trans r (Comp (flip r') r) r'

Equations

• Relation.instTransCompFlipOfDompeq = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransCompFlipOfDompeq_1 {α : Type u_1} {β : Type u_2} {r r' : α → β → Prop} [Dompeq r r'] : Trans (Comp r (flip r')) r r'

Equations

• Relation.instTransCompFlipOfDompeq_1 = { trans := ⋯ }

theorem Relation.dompeq_apply {α : Type u_1} {β : Type u_2} {a b : α} {x y : β} {r r' : α → β → Prop} [Dompeq r r'] (hr'ax : r' a x) (hrbx : r b x) (hray : r a y) : r' b y

theorem Relation.dompeq_left_iff {α : Type u_1} {β : Type u_2} {a b : α} {x y : β} {r : α → β → Prop} [Dompeq r r] (hrax : r a x) (hrbx : r b x) : r a y ↔ r b y

theorem Relation.dompeq_right_iff {α : Type u_1} {β : Type u_2} {a b : α} {x y : β} {r : α → β → Prop} [Dompeq r r] (hrax : r a x) (hray : r a y) : r b x ↔ r b y

def Relation.fiber {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (x : β) : Set α

Equations

• Relation.fiber r x = {a : α | r a x}

@[simp]

theorem Relation.mem_fiber_iff {α : Type u_1} {β : Type u_2} {a : α} {x : β} (r : α → β → Prop) : a ∈ fiber r x ↔ r a x

@[simp]

theorem Relation.fiber_empty {α : Type u_1} {β : Type u_2} {x : β} {r : α → β → Prop} : fiber r x = ∅ ↔ x ∉ codomain r

theorem Relation.fiber_eq_or_disjoint {α : Type u_1} {β : Type u_2} {x y : β} {r : α → β → Prop} [Dompeq r r] : fiber r x = fiber r y ∨ Disjoint (fiber r x) (fiber r y)

theorem Relation.fiber_eq_of_mem {α : Type u_1} {β : Type u_2} {a : α} {x y : β} {r : α → β → Prop} [Dompeq r r] (hrax : r a x) (hray : r a y) : fiber r x = fiber r y

def Relation.image {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (S : Set α) : Set β

Equations

• Relation.image r S = {x : β | ∃ a ∈ S, r a x}

def Relation.preimage {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (S : Set β) : Set α

Equations

• Relation.preimage r S = {a : α | ∃ x ∈ S, r a x}

@[simp]

theorem Relation.image_flip {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (S : Set β) : image (flip r) S = preimage r S

@[simp]

theorem Relation.preimage_flip {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (S : Set α) : preimage (flip r) S = image r S

@[simp]

theorem Relation.mem_image_iff {α : Type u_1} {β : Type u_2} {x : β} (r : α → β → Prop) (S : Set α) : x ∈ image r S ↔ ∃ a ∈ S, r a x

@[simp]

theorem Relation.mem_preimage_iff {α : Type u_1} {β : Type u_2} {a : α} (r : α → β → Prop) (S : Set β) : a ∈ preimage r S ↔ ∃ x ∈ S, r a x

@[simp]

theorem Relation.sUnion_fiber {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (S : Set β) : ⋃₀ (fiber r '' S) = preimage r S

@[simp]

theorem Relation.image_domain {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : image r (domain r) = codomain r

@[simp]

theorem Relation.preimage_codomain {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : preimage r (codomain r) = domain r

@[simp]

theorem Relation.image_mono {α : Type u_1} {β : Type u_2} {r r' : α → β → Prop} (h : r ≤ r') (S : Set α) : image r S ⊆ image r' S

@[simp]

theorem Relation.preimage_mono {α : Type u_1} {β : Type u_2} {r r' : α → β → Prop} (h : r ≤ r') (S : Set β) : preimage r S ⊆ preimage r' S

class Relation.IsLeftTotal {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : Prop

• is_left_total (a : α) : ∃ (x : β), r a x

theorem Relation.left_total {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [IsLeftTotal r] (a : α) : ∃ (x : β), r a x

@[simp]

theorem Relation.domain_univ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [IsLeftTotal r] : domain r = Set.univ

class Relation.IsRightTotal {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : Prop

• is_right_total (x : β) : ∃ (a : α), r a x

theorem Relation.right_total {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [IsRightTotal r] (x : β) : ∃ (a : α), r a x

@[simp]

theorem Relation.codomain_univ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [IsRightTotal r] : codomain r = Set.univ

class Relation.IsTotal {α : Type u_1} {β : Type u_2} (r : α → β → Prop) extends Relation.IsLeftTotal r, Relation.IsRightTotal r : Prop

• is_left_total (a : α) : ∃ (x : β), r a x
• is_right_total (x : β) : ∃ (a : α), r a x

class Relation.IsLeftUnique {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : Prop

• is_left_unique (a : α) (x y : β) : r a x → r a y → x = y

theorem Relation.left_unique {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [IsLeftUnique r] (a : α) (x y : β) : r a x → r a y → x = y

class Relation.IsRightUnique {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : Prop

• is_right_unique (a b : α) (x : β) : r a x → r b x → a = b

theorem Relation.right_unique {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [IsRightUnique r] (a b : α) (x : β) : r a x → r b x → a = b

class Relation.IsUnique {α : Type u_1} {β : Type u_2} (r : α → β → Prop) extends Relation.IsLeftUnique r, Relation.IsRightUnique r : Prop

• is_left_unique (a : α) (x y : β) : r a x → r a y → x = y
• is_right_unique (a b : α) (x : β) : r a x → r b x → a = b

def Relation.fibers {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : Set (Set α)

Equations

• Relation.fibers r = Relation.fiber r '' Relation.codomain r

theorem Relation.fiber_mem_fibers_of_mem_codomain {α : Type u_1} {β : Type u_2} {x : β} {r : α → β → Prop} (hx : x ∈ codomain r) : fiber r x ∈ fibers r

theorem Relation.fiber_mem_fibers {α : Type u_1} {β : Type u_2} {a : α} {x : β} {r : α → β → Prop} (hx : r a x) : fiber r x ∈ fibers r

@[simp]

theorem Relation.mem_fibers_iff {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (S : Set α) : S ∈ fibers r ↔ ∃ x ∈ codomain r, fiber r x = S

theorem Relation.emptySet_notMem_fibers {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : ∅ ∉ fibers r

theorem Relation.nonempty_of_mem_fibers {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {S : Set α} (hS : S ∈ fibers r) : S.Nonempty

@[simp]

theorem Relation.sUnion_fibers {α : Type u_1} {β : Type u_2} (r : α → β → Prop) : ⋃₀ fibers r = domain r

theorem Relation.fibers_pairwiseDisjoint' {α : Type u_1} {β : Type u_2} {r : α → β → Prop} [IsLeftUnique r] : (fibers r).PairwiseDisjoint id

theorem Relation.fibers_pairwiseDisjoint {α : Type u_1} {β : Type u_2} {r : α → β → Prop} [Dompeq r r] : (fibers r).PairwiseDisjoint id

@[instance_reducible]

instance Relation.instHasSubsetForallForallProp_matroid {α : Type u_1} {β : Type u_2} : HasSubset (α → β → Prop)

Equations

• Relation.instHasSubsetForallForallProp_matroid = { Subset := fun (r s : α → β → Prop) => Relation.fibers r ⊆ Relation.fibers s }

instance Relation.instIsPreorderForallForallPropSubset_matroid {α : Type u_1} {β : Type u_2} : IsPreorder (α → β → Prop) fun (x1 x2 : α → β → Prop) => x1 ⊆ x2

def Relation.leftRestrict {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (S : Set α) : α → β → Prop

Equations

• Relation.leftRestrict r S x y = (r x y ∧ x ∈ S)

def Relation.rightRestrict {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (S : Set β) : α → β → Prop

Equations

• Relation.rightRestrict r S x y = (r x y ∧ y ∈ S)

def Relation.leftResidual {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : α → β → Prop) (s : α → γ → Prop) : β → γ → Prop

Equations

• Relation.leftResidual r s = (Relation.Comp (flip r) sᶜ)ᶜ

def Relation.rightResidual {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : α → β → Prop) (s : γ → β → Prop) : α → γ → Prop

Equations

• Relation.rightResidual r s = (Relation.Comp rᶜ (flip s))ᶜ

@[simp]

theorem Relation.leftResidual_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : β} {u : γ} {r : α → β → Prop} {t : α → γ → Prop} : leftResidual r t x u ↔ ∀ (a : α), r a x → t a u

@[simp]

theorem Relation.rightResidual_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {a : α} {u : γ} {r : α → β → Prop} {s : γ → β → Prop} : rightResidual r s a u ↔ ∀ (x : β), s u x → r a x

theorem Relation.comp_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : α → β → Prop) (s : β → γ → Prop) (t : α → γ → Prop) [Trans r s t] : Comp r s ≤ t

theorem Relation.Schroder_leftResidual {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {s : β → γ → Prop} {t : α → γ → Prop} : Comp r s ≤ t ↔ s ≤ leftResidual r t

theorem Relation.le_leftResidual {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : α → β → Prop) (s : β → γ → Prop) (t : α → γ → Prop) [Trans r s t] : s ≤ leftResidual r t

theorem Relation.Schroder_rightResidual {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {s : β → γ → Prop} {t : α → γ → Prop} : Comp r s ≤ t ↔ r ≤ rightResidual t s

theorem Relation.le_rightResidual {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {s : β → γ → Prop} {t : α → γ → Prop} [Trans r s t] : r ≤ rightResidual t s

theorem Relation.left_rw {α : Type u_1} {β : Type u_2} {a b : α} {c : β} {r : α → α → Prop} [Std.Symm r] (s : α → β → Prop) [Trans r s s] (hr : r a b) : s a c ↔ s b c

theorem Relation.right_rw {α : Type u_1} {β : Type u_2} {a : α} {b c : β} {r : β → β → Prop} [Std.Symm r] (s : α → β → Prop) [Trans s r s] (hs : r b c) : s a b ↔ s a c

@[instance_reducible]

instance Relation.instTransBotForallForallProp_matroid {α : Type u_1} {β : Type u_2} {r : α → α → Prop} : Trans r ⊥ ⊥

Equations

• Relation.instTransBotForallForallProp_matroid = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransBotForallForallProp_matroid_1 {α : Type u_1} {β : Type u_2} {r : α → β → Prop} : Trans ⊥ r r

Equations

• Relation.instTransBotForallForallProp_matroid_1 = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransComp_matroid {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s s' : α → β → Prop} [Trans r s s'] : Trans r (Comp r s) (Comp r s')

Equations

• Relation.instTransComp_matroid = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransCompOfIsTrans_matroid {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : α → β → Prop} [IsTrans α r] : Trans r (Comp r s) (Comp r s)

Equations

• Relation.instTransCompOfIsTrans_matroid = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransCompOfIsTrans_matroid_1 {α : Type u_1} {β : Type u_2} {s : α → β → Prop} {r : β → β → Prop} [IsTrans β r] : Trans (Comp s r) r (Comp s r)

Equations

• Relation.instTransCompOfIsTrans_matroid_1 = { trans := ⋯ }

@[simp]

theorem Relation.comp_bot {α : Type u_1} {β : Type u_2} {γ : Type u_5} (r : α → β → Prop) : Comp r ⊥ = ⊥

@[simp]

theorem Relation.bot_comp {α : Type u_1} {β : Type u_2} {γ : Type u_5} (r : β → γ → Prop) : Comp ⊥ r = ⊥

instance Relation.instReflTopForallForallProp_matroid {α : Type u_1} : Std.Refl ⊤

instance Relation.instSymmTopForallForallProp_matroid {α : Type u_1} : Std.Symm ⊤

instance Relation.instIsTransTopForallForallProp_matroid {α : Type u_1} : IsTrans α ⊤

instance Relation.instSymmBotForallForallProp_matroid {α : Type u_1} : Std.Symm ⊥

instance Relation.instIsTransBotForallForallProp_matroid {α : Type u_1} : IsTrans α ⊥

instance Relation.instReflOnFun_matroid {α : Type u_1} {β : Type u_2} {f : β → α} {r : α → α → Prop} [Std.Refl r] : Std.Refl (Function.onFun r f)

instance Relation.instSymmOnFun_matroid {α : Type u_1} {β : Type u_2} {f : β → α} {r : α → α → Prop} [Std.Symm r] : Std.Symm (Function.onFun r f)

instance Relation.instIsTransOnFun_matroid {α : Type u_1} {β : Type u_2} {f : β → α} {r : α → α → Prop} [IsTrans α r] : IsTrans β (Function.onFun r f)

@[instance_reducible]

instance Relation.instTransOfIsTransOfDompeq {α : Type u_1} {r s : α → α → Prop} [IsTrans α r] [Dompeq r s] : Trans r s s

Equations

• Relation.instTransOfIsTransOfDompeq = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransOfIsTransOfDompeq_1 {α : Type u_1} {r s : α → α → Prop} [IsTrans α r] [Dompeq r s] : Trans s r s

Equations

• Relation.instTransOfIsTransOfDompeq_1 = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransOfSymm_matroid {α : Type u_1} {r s : α → α → Prop} [Std.Symm r] [Std.Symm s] [Trans r s s] : Trans s r s

Equations

• Relation.instTransOfSymm_matroid = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransOfSymm_matroid_1 {α : Type u_1} {r s : α → α → Prop} [Std.Symm r] [Std.Symm s] [Trans s r s] : Trans r s s

Equations

• Relation.instTransOfSymm_matroid_1 = { trans := ⋯ }

instance Relation.instSymmMaxForallForallProp_matroid {α : Type u_1} {r s : α → α → Prop} [Std.Symm r] [Std.Symm s] : Std.Symm (r ⊔ s)

instance Relation.instSymmMinForallForallProp_matroid {α : Type u_1} {r s : α → α → Prop} [Std.Symm r] [Std.Symm s] : Std.Symm (r ⊓ s)

instance Relation.instReflFlip_matroid {α : Type u_1} {r : α → α → Prop} [Std.Refl r] : Std.Refl (flip r)

instance Relation.instSymmFlip_matroid {α : Type u_1} {r : α → α → Prop} [Std.Symm r] : Std.Symm (flip r)

instance Relation.instIsTransFlip_matroid {α : Type u_1} {r : α → α → Prop} [IsTrans α r] : IsTrans α (flip r)

instance Relation.instAntisymmFlip_matroid {α : Type u_1} {r : α → α → Prop} [Std.Antisymm r] : Std.Antisymm (flip r)

instance Relation.instIsPreorderFlip_matroid {α : Type u_1} {r : α → α → Prop} [IsPreorder α r] : IsPreorder α (flip r)

instance Relation.instIsLinearOrderFlip_matroid {α : Type u_1} {r : α → α → Prop} [IsLinearOrder α r] : IsLinearOrder α (flip r)

theorem Relation.sSup_symmtric {α : Type u_1} {s : Set (α → α → Prop)} (hs : ∀ r ∈ s, Std.Symm r) : Std.Symm (sSup s)

theorem Relation.sInf_symmtric {α : Type u_1} {s : Set (α → α → Prop)} (hs : ∀ r ∈ s, Std.Symm r) : Std.Symm (sInf s)

instance Relation.instSymmISupForallForallProp_matroid {α : Type u_1} {ι : Type u_4} {s : ι → α → α → Prop} [∀ (i : ι), Std.Symm (s i)] : Std.Symm (⨆ (i : ι), s i)

instance Relation.instSymmIInfForallForallProp_matroid {α : Type u_1} {ι : Type u_4} {s : ι → α → α → Prop} [∀ (i : ι), Std.Symm (s i)] : Std.Symm (⨅ (i : ι), s i)

theorem Relation.sInf_transitive {α : Type u_1} {s : Set (α → α → Prop)} (hs : ∀ r ∈ s, IsTrans α r) : IsTrans α (sInf s)

instance Relation.instIsTransIInfForallForallProp_matroid {α : Type u_1} {ι : Type u_4} {s : ι → α → α → Prop} [∀ (i : ι), IsTrans α (s i)] : IsTrans α (⨅ (i : ι), s i)

theorem Relation.domain_eq_codomain {α : Type u_1} (r : α → α → Prop) [Std.Symm r] : domain r = codomain r

instance Relation.instIsTransMinForallForallProp_matroid {α : Type u_1} {r s : α → α → Prop} [IsTrans α r] [IsTrans α s] : IsTrans α (r ⊓ s)

instance Relation.instIsTransFlip_matroid_1 {α : Type u_1} {r : α → α → Prop} [IsTrans α r] : IsTrans α (flip r)

theorem Relation.transitive_of_le_eq {α : Type u_1} (r : α → α → Prop) (hr : r ≤ fun (x1 x2 : α) => x1 = x2) : IsTrans α r

def Relation.SymmClosure {α : Type u_1} : ClosureOperator (α → α → Prop)

Equations

• Relation.SymmClosure = { toFun := fun (r : α → α → Prop) => r ⊔ flip r, monotone' := ⋯, le_closure' := ⋯, idempotent' := ⋯, isClosed_iff := ⋯ }

@[simp]

theorem Relation.symmClosure_apply {α : Type u_1} (r : α → α → Prop) (a b : α) : SymmClosure r a b ↔ r a b ∨ r b a

instance Relation.instSymmCoeClosureOperatorForallForallPropSymmClosure {α : Type u_1} {r : α → α → Prop} : Std.Symm (SymmClosure r)

theorem Relation.SymmClosure.symm {α : Type u_1} {a b : α} {r : α → α → Prop} (hr : SymmClosure r a b) : SymmClosure r b a

@[simp]

theorem Relation.symmClosure_domain {α : Type u_1} (r : α → α → Prop) : domain (SymmClosure r) = domain r ∪ codomain r

@[simp]

theorem Relation.symmClosure_codomain {α : Type u_1} (r : α → α → Prop) : codomain (SymmClosure r) = domain r ∪ codomain r

@[simp]

theorem Relation.symmClosure_eq_self {α : Type u_1} (r : α → α → Prop) [Std.Symm r] : SymmClosure r = r

def Relation.TransClosure {α : Type u_1} : ClosureOperator (α → α → Prop)

Equations

• Relation.TransClosure = { toFun := Relation.TransGen, monotone' := ⋯, le_closure' := ⋯, idempotent' := ⋯, IsClosed := IsTrans α, isClosed_iff := ⋯ }

instance Relation.instIsTransCoeClosureOperatorForallForallPropTransClosure {α : Type u_1} {r : α → α → Prop} : IsTrans α (TransClosure r)

instance Relation.instSymmCoeClosureOperatorForallForallPropTransClosure {α : Type u_1} {r : α → α → Prop} [Std.Symm r] : Std.Symm (TransClosure r)

@[simp]

theorem Relation.transClosure_eq_self {α : Type u_1} (r : α → α → Prop) [IsTrans α r] : TransClosure r = r

theorem Relation.transClosure_eq_self_of_le_eq {α : Type u_1} {r : α → α → Prop} (hr : r ≤ fun (x1 x2 : α) => x1 = x2) : TransClosure r = r

@[simp]

theorem Relation.transClosure_eq {α : Type u_1} : TransClosure Eq = Eq

theorem Relation.transClosure_le_of_le_trans {α : Type u_1} {r s : α → α → Prop} (hr : r ≤ s) [IsTrans α s] : TransClosure r ≤ s

theorem Relation.transClosure_le_domp_of_le_trans {α : Type u_1} {r s : α → α → Prop} (hr : r ≤ s) [IsTrans α s] : TransClosure r ≤ Domp s r

@[simp]

theorem Relation.transClosure_domain {α : Type u_1} (r : α → α → Prop) : domain (TransClosure r) = domain r

@[simp]

theorem Relation.transClosure_codomain {α : Type u_1} (r : α → α → Prop) : codomain (TransClosure r) = codomain r

theorem Relation.transClosure_exists_single_head {α : Type u_1} {a b : α} (r : α → α → Prop) (h : TransClosure r a b) : ∃ (c : α), r a c

theorem Relation.transClosure_exists_single_tail {α : Type u_1} {a b : α} (r : α → α → Prop) (h : TransClosure r a b) : ∃ (c : α), r c b

class Relation.foo {α : Type u_1} (r : α → α → Prop) : Prop

Minimal assumption (that I can think of) for transGen_self_iff.

• isfoo ⦃a b : α⦄ : r a b → r b b

theorem Relation.refl_of_right {α : Type u_1} {a b : α} {r : α → α → Prop} [foo r] (h : r a b) : r b b

theorem Relation.refl_of_left {α : Type u_1} {a b : α} {r : α → α → Prop} [foo (flip r)] (h : r a b) : r a a

instance Relation.instFooOfSymmOfIsTrans {α : Type u_1} {r : α → α → Prop} [Std.Symm r] [IsTrans α r] : foo r

instance Relation.instFooFlipOfSymm {α : Type u_1} {r : α → α → Prop} [Std.Symm r] [foo r] : foo (flip r)

instance Relation.instFooMaxForallForallProp {α : Type u_1} {r s : α → α → Prop} [foo r] [foo s] : foo (r ⊔ s)

theorem Relation.foo_sSup {α : Type u_1} {s : Set (α → α → Prop)} (hs : ∀ r ∈ s, foo r) : foo (sSup s)

instance Relation.instFooISupForallForallProp {α : Type u_1} {ι : Type u_4} {r : ι → α → α → Prop} [H : ∀ (i : ι), foo (r i)] : foo (⨆ (i : ι), r i)

instance Relation.instFooMinForallForallProp {α : Type u_1} {r s : α → α → Prop} [foo r] [foo s] : foo (r ⊓ s)

theorem Relation.foo_sInf {α : Type u_1} {s : Set (α → α → Prop)} (hs : ∀ r ∈ s, foo r) : foo (sInf s)

instance Relation.instFooIInfForallForallProp {α : Type u_1} {ι : Type u_4} {r : ι → α → α → Prop} [H : ∀ (i : ι), foo (r i)] : foo (⨅ (i : ι), r i)

@[simp]

theorem Relation.transClosure_self_iff {α : Type u_1} {a : α} {r : α → α → Prop} [foo r] : TransClosure r a a ↔ r a a

instance Relation.instDompeqOfSymmOfIsTrans {α : Type u_1} {r : α → α → Prop} [Std.Symm r] [IsTrans α r] : Dompeq r r

theorem Relation.comp_idem_left {α : Type u_1} {β : Type u_2} (r : α → α → Prop) [IsTrans α r] [foo r] (s : α → β → Prop) : Comp r (Comp r s) = Comp r s

theorem Relation.comp_idem_right {α : Type u_1} {β : Type u_2} (r : α → α → Prop) [IsTrans α r] [foo (flip r)] (s : β → α → Prop) : Comp (Comp s r) r = Comp s r

theorem Relation.comp_self {α : Type u_1} (r : α → α → Prop) [IsTrans α r] [foo r] : Comp r r = r

instance Relation.instSymmDomp {α : Type u_1} {r s : α → α → Prop} [Std.Symm r] [Std.Symm s] : Std.Symm (Domp r s)

instance Relation.instIsTransDompOfSymmOfTrans {α : Type u_1} {r s : α → α → Prop} [Std.Symm r] [IsTrans α s] [H : Trans s r s] : IsTrans α (Domp r s)

@[instance_reducible]

instance Relation.instTransDompOfIsTrans {α : Type u_1} {r s : α → α → Prop} [IsTrans α r] : Trans r (Domp r s) (Domp r s)

Equations

• Relation.instTransDompOfIsTrans = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransDompOfIsTrans_1 {α : Type u_1} {r s : α → α → Prop} [IsTrans α r] : Trans (Domp r s) r (Domp r s)

Equations

• Relation.instTransDompOfIsTrans_1 = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransOfDompeqOfIsTrans {α : Type u_1} {r s : α → α → Prop} [Dompeq r s] [IsTrans α r] : Trans r s s

Equations

• Relation.instTransOfDompeqOfIsTrans = { trans := ⋯ }

@[instance_reducible]

instance Relation.instTransOfDompeqOfIsTrans_1 {α : Type u_1} {r s : α → α → Prop} [Dompeq r s] [IsTrans α r] : Trans s r s

Equations

• Relation.instTransOfDompeqOfIsTrans_1 = { trans := ⋯ }

def Relation.restrict {α : Type u_1} (r : α → α → Prop) (S : Set α) : α → α → Prop

Equations

• Relation.restrict r S x y = (r x y ∧ x ∈ S ∧ y ∈ S)

theorem Relation.restrict.left_mem {α : Type u_1} {a b : α} {r : α → α → Prop} {S : Set α} (h : restrict r S a b) : a ∈ S

theorem Relation.restrict.right_mem {α : Type u_1} {a b : α} {r : α → α → Prop} {S : Set α} (h : restrict r S a b) : b ∈ S

theorem Relation.restrict_mono {α : Type u_1} {r s : α → α → Prop} (h : r ≤ s) (S : Set α) : restrict r S ≤ restrict s S

theorem Relation.restrict_le {α : Type u_1} (r : α → α → Prop) (S : Set α) : restrict r S ≤ r

theorem Relation.restrict_subset {α : Type u_1} (r : α → α → Prop) {S T : Set α} (h : S ⊆ T) : restrict r S ≤ restrict r T

instance Relation.instSymmRestrict {α : Type u_1} {r : α → α → Prop} [Std.Symm r] {S : Set α} : Std.Symm (restrict r S)

theorem Relation.restrict_eq_self {α : Type u_1} (r : α → α → Prop) [Std.Symm r] {S : Set α} (hS : domain r ⊆ S) : restrict r S = r

theorem Relation.restrict_eq_iff {α : Type u_1} (r : α → α → Prop) [Std.Symm r] (S : Set α) : restrict r S = r ↔ domain r ⊆ S

@[simp]

theorem Relation.restrict_inter {α : Type u_1} (r : α → α → Prop) (S T : Set α) : restrict r (S ∩ T) = restrict r S ⊓ restrict r T

@[simp]

theorem Relation.restrict_inf {α : Type u_1} (r s : α → α → Prop) (S : Set α) : restrict (r ⊓ s) S = restrict r S ⊓ restrict s S

@[simp]

theorem Relation.restrict_sup {α : Type u_1} (r s : α → α → Prop) (S : Set α) : restrict (r ⊔ s) S = restrict r S ⊔ restrict s S

@[simp]

theorem Relation.restrict_singleton_of_not {α : Type u_1} (r : α → α → Prop) (a : α) (hra : ¬r a a) : restrict r {a} = fun (x x_1 : α) => False

@[simp]

theorem Relation.restrict_singleton_of_refl {α : Type u_1} (r : α → α → Prop) [Std.Refl r] (a : α) : restrict r {a} = fun (x y : α) => x = a ∧ y = a

theorem List.IsChain.head_rel {α : Type u_5} {r : α → α → Prop} [IsPreorder α r] {l : List α} (h : IsChain r l) (hne : l ≠ []) (x : α) : x ∈ l → r (l.head hne) x

theorem List.IsChain.rel_last {α : Type u_5} {r : α → α → Prop} [IsPreorder α r] {l : List α} (h : IsChain r l) (hne : l ≠ []) (x : α) : x ∈ l → r x (l.getLast hne)

theorem List.IsChain.eq_head_of_antisymm {α : Type u_5} {r : α → α → Prop} [IsPartialOrder α r] {l : List α} (h : IsChain r l) (hne : l ≠ []) (hend : l.head hne = l.getLast hne) (x : α) : x ∈ l → x = l.head hne

theorem List.IsChain.antisymm {α : Type u_5} {r : α → α → Prop} [IsPartialOrder α r] {l : List α} (h : IsChain r l) (hend : l.head = l.getLast) (x : α) : x ∈ l → ∀ y ∈ l, x = y