inductive SymmGen {α : Type u_1} (r : Rel α α) : Rel α α

• fw_step: ∀ {α : Type u_1} {r : Rel α α} {x y : α}, r x y → SymmGen r x y
• bw_step: ∀ {α : Type u_1} {r : Rel α α} {x y : α}, r y x → SymmGen r x y

def Rel.union {α : Type u_1} {β : Type u_2} : Rel α β → Rel α β → Rel α β

Equations

• r₁.union r₂ x y = (r₁ x y ∨ r₂ x y)

instance Rel.instUnion {α : Type u_1} {β : Type u_2} : Union (Rel α β)

Equations

• Rel.instUnion = { union := Rel.union }

def Rel.union_comm {α : Type u_1} (a b : Rel α α) : a ∪ b = b ∪ a

Equations

• ⋯ = ⋯

def Rel.union_left {α : Type u_1} {a b : Rel α α} (x y : α) : a x y → (a ∪ b) x y

Equations

• ⋯ = ⋯

def Rel.union_right {α : Type u_1} {a b : Rel α α} (x y : α) : b x y → (a ∪ b) x y

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev Rel.reflTransGen {α : Type u_1} : Rel α α → Rel α α

Equations

• Rel.reflTransGen = Relation.ReflTransGen

@[reducible, inline]

abbrev Rel.eqvGen {α : Type u_1} : Rel α α → Rel α α

Equations

• Rel.eqvGen = Relation.EqvGen

@[reducible, inline]

abbrev Rel.transGen {α : Type u_1} : Rel α α → Rel α α

Equations

• Rel.transGen = Relation.TransGen

@[reducible, inline]

abbrev Rel.reflGen {α : Type u_1} : Rel α α → Rel α α

Equations

• Rel.reflGen = Relation.ReflGen

theorem Relation.ReflTransGen.to_equiv {α : Type u_1} {r : Rel α α} {a b : α} (h : Relation.ReflTransGen r a b) : Relation.EqvGen r a b

The reflexive-transitive closure of a relation is a subset of the equivalence closure.

def Thesis.«term_∗» : Lean.TrailingParserDescr

Equations

• Thesis.«term_∗» = Lean.ParserDescr.trailingNode `Thesis.«term_∗» 1024 1024 (Lean.ParserDescr.symbol "∗")

def Thesis.«term_≡» : Lean.TrailingParserDescr

Equations

• Thesis.«term_≡» = Lean.ParserDescr.trailingNode `Thesis.«term_≡» 1024 1024 (Lean.ParserDescr.symbol "≡")

def Thesis.«term_⁼» : Lean.TrailingParserDescr

Equations

• Thesis.«term_⁼» = Lean.ParserDescr.trailingNode `Thesis.«term_⁼» 1024 1024 (Lean.ParserDescr.symbol "⁼")

def Thesis.«term_⁺» : Lean.TrailingParserDescr

Equations

• Thesis.«term_⁺» = Lean.ParserDescr.trailingNode `Thesis.«term_⁺» 1024 1024 (Lean.ParserDescr.symbol "⁺")

@[simp]

theorem Thesis.star_inv_iff_inv_star {α : Type u_1} {r : Rel α α} {x y : α} : r.inv∗ x y ↔ r∗ y x

Taking the inverse of a relation commutes with reflexive-transitive closure.

def Thesis.star_inv_of_inv_star {α : Type u_1} {r : Rel α α} {x y : α} : r.inv∗ x y → r∗ y x

Equations

• ⋯ = ⋯

def Thesis.inv_star_of_star_inv {α : Type u_1} {r : Rel α α} {x y : α} : r∗ y x → r.inv∗ x y

Equations

• ⋯ = ⋯

@[simp]

theorem Thesis.trans_inv_iff_inv_trans {α : Type u_1} {r : Rel α α} {x y : α} : r.inv⁺ x y ↔ r⁺ y x

Taking the inverse of a relation commutes with transitive closure.

def Thesis.trans_inv_of_inv_trans {α : Type u_1} {r : Rel α α} {x y : α} : r.inv⁺ x y → r⁺ y x

Equations

• ⋯ = ⋯

def Thesis.inv_trans_of_trans_inv {α : Type u_1} {r : Rel α α} {x y : α} : r⁺ y x → r.inv⁺ x y

Equations

• ⋯ = ⋯