Basic properties of relations

TODO:

Many of the results here could be upstreamed to Mathlib. In particular:

• ReflGen.le_reflGen and relatives,
• ReflGen.to_eqvGen and relatives.

theorem WellFounded.ofTransGen {α : Type u_1} {r : α → α → Prop} (trans_wf : WellFounded (Relation.TransGen r)) : WellFounded r

@[simp]

theorem WellFounded.iff_transGen {α : Type u_1} {r : α → α → Prop} : WellFounded (Relation.TransGen r) ↔ WellFounded r

@[implicit_reducible]

def Relation.transLeftRight {α : Type u_1} (s s' r : α → α → Prop) [IsTrans α r] (h : s ≤ r) (h' : s' ≤ r) : Trans s s' r

A pair of subrelations lifts to transitivity on the relation.

Equations

• Relation.transLeftRight s s' r h h' = { trans := ⋯ }

@[implicit_reducible]

def Relation.transLeft {α : Type u_1} (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans s r r

A subrelation lifts to transitivity on the left of the relation.

Equations

• Relation.transLeft s r h = { trans := ⋯ }

@[implicit_reducible]

def Relation.transRight {α : Type u_1} (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans r s r

A subrelation lifts to transitivity on the right of the relation.

Equations

• Relation.transRight s r h = { trans := ⋯ }

theorem Relation.comp_le_comp {α : Type u_1} {s s' r r' : α → α → Prop} (hs : s ≤ s') (hr : r ≤ r') : Comp s r ≤ Comp s' r'

theorem Relation.comp_self_le {α : Type u_1} (r : α → α → Prop) [IsTrans α r] : Comp r r ≤ r

theorem Relation.swap_le_iff_le_swap {α : Type u_1} {r₁ r₂ : α → α → Prop} : Function.swap r₁ ≤ r₂ ↔ r₁ ≤ Function.swap r₂

theorem Relation.ReflGen.le_reflGen {α : Type u_1} {r : α → α → Prop} : r ≤ ReflGen r

theorem Relation.ReflGen.to_eqvGen {α : Type u_1} {r : α → α → Prop} {a b : α} (h : ReflGen r a b) : EqvGen r a b

theorem Relation.TransGen.le_transGen {α : Type u_1} {r : α → α → Prop} : r ≤ TransGen r

theorem Relation.TransGen.to_eqvGen {α : Type u_1} {r : α → α → Prop} {a b : α} (h : TransGen r a b) : EqvGen r a b

theorem Relation.ReflTransGen.to_eqvGen {α : Type u_1} {r : α → α → Prop} {a b : α} (h : ReflTransGen r a b) : EqvGen r a b

theorem Relation.SymmGen.le_symmGen {α : Type u_1} {r : α → α → Prop} : r ≤ SymmGen r

theorem Relation.SymmGen.to_eqvGen {α : Type u_1} {r : α → α → Prop} {a b : α} (h : SymmGen r a b) : EqvGen r a b

@[simp]

theorem Relation.sup_swap_eq_symmGen {α : Type u_1} {r : α → α → Prop} : r ⊔ Function.swap r = SymmGen r

theorem Relation.EqvGen.le_eqvGen {α : Type u_1} {r : α → α → Prop} : r ≤ EqvGen r

theorem Equivalence.eqvGen_le {α : Type u_1} {r₁ r₂ : α → α → Prop} (h : Equivalence r₂) (hle : r₁ ≤ r₂) : Relation.EqvGen r₁ ≤ r₂

theorem Relation.Join.single {α : Type u_1} {r : α → α → Prop} {a b : α} [Std.Refl r] (h : r a b) : Join r a b

@[simp]

theorem Relation.join₂_eq_join {α : Type u_1} {r : α → α → Prop} : Join₂ r r = Join r

theorem Relation.join₂_eq_comp_swap {α : Type u_1} {r₁ r₂ : α → α → Prop} : Join₂ r₁ r₂ = Comp r₁ (Function.swap r₂)

instance Relation.instReflJoin₂ {α : Type u_1} {r₁ r₂ : α → α → Prop} [Std.Refl r₁] [Std.Refl r₂] : Std.Refl (Join₂ r₁ r₂)

theorem Relation.Join₂.single_left {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} [Std.Refl r₂] (h : r₁ a b) : Join₂ r₁ r₂ a b

theorem Relation.Join₂.single_right {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} [Std.Refl r₁] (h : r₂ a b) : Join₂ r₁ r₂ b a

theorem Relation.Join₂.join₂_le {α : Type u_1} {r r₁ r₂ : α → α → Prop} [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : Function.swap r₂ ≤ r) : Join₂ r₁ r₂ ≤ r

theorem Relation.Join₂.swap_iff {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} : Join₂ r₁ r₂ b a ↔ Join₂ r₂ r₁ a b

theorem Relation.Join₂.mono {α : Type u_1} {r₁ r₂ r₁' r₂' : α → α → Prop} (h₁ : r₁ ≤ r₁') (h₂ : r₂ ≤ r₂') : Join₂ r₁ r₂ ≤ Join₂ r₁' r₂'

@[deprecated refl (since := "2026-09-07")]

theorem Relation.MJoin.refl {α : Type u_1} {r : α → α → Prop} (a : α) : MJoin r a a

@[deprecated Relation.Join.single (since := "2026-09-07")]

theorem Relation.MJoin.single {α : Type u_1} {r : α → α → Prop} {a b : α} (h : ReflTransGen r a b) : MJoin r a b

theorem Equivalence.join_reflTransGen_le {α : Type u_1} {r₁ r₂ : α → α → Prop} (h : Equivalence r₂) (hle : r₁ ≤ r₂) : Relation.Join (Relation.ReflTransGen r₁) ≤ r₂

theorem Relation.join_reflTransGen_le_eqvGen {α : Type u_1} {r : α → α → Prop} : Join (ReflTransGen r) ≤ EqvGen r

theorem Relation.join₂_reflTransGen_le {α : Type u_1} {r r₁ r₂ : α → α → Prop} [Std.Refl r] [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : Function.swap r₂ ≤ r) : Join₂ (ReflTransGen r₁) (ReflTransGen r₂) ≤ r

theorem Relation.join₂_reflTransGen_le_of_isEquiv {α : Type u_1} {r r₁ r₂ : α → α → Prop} [IsEquiv α r] (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : Join₂ (ReflTransGen r₁) (ReflTransGen r₂) ≤ r

theorem Equivalence.join₂_reflTransGen_le {α : Type u_1} {r r₁ r₂ : α → α → Prop} (h : Equivalence r) (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : Relation.Join₂ (Relation.ReflTransGen r₁) (Relation.ReflTransGen r₂) ≤ r

theorem Relation.left_le_join₂_reflTransGen {α : Type u_1} {r₁ r₂ : α → α → Prop} : r₁ ≤ Join₂ (ReflTransGen r₁) (ReflTransGen r₂)

theorem Relation.swap_right_le_join₂_reflTransGen {α : Type u_1} {r₁ r₂ : α → α → Prop} : Function.swap r₂ ≤ Join₂ (ReflTransGen r₁) (ReflTransGen r₂)

theorem Relation.reflTransGen_mono_closed {α : Type u_1} {r₁ r₂ : α → α → Prop} (h₁ : r₁ ≤ r₂) (h₂ : r₂ ≤ ReflTransGen r₁) : ReflTransGen r₁ = ReflTransGen r₂

If a relation is squeezed by a relation and its multi-step closure, they are multi-step equal

@[deprecated Relation.ReflGen.stdSymm (since := "2026-09-03")]

theorem Relation.ReflGen.symmGen_symm {α : Type u_1} {r : α → α → Prop} {a b : α} : ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a

@[simp]

theorem Relation.reflTransGen_symmGen {α : Type u_1} {r : α → α → Prop} : ReflTransGen (SymmGen r) = EqvGen r

theorem Relation.join_inl {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} (r₁_ab : r₁ a b) : (r₁ ⊔ r₂) a b

theorem Relation.join_inr {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} (r₂_ab : r₂ a b) : (r₁ ⊔ r₂) a b

theorem Relation.join_inl_reflTransGen {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} (r₁_ab : ReflTransGen r₁ a b) : ReflTransGen (r₁ ⊔ r₂) a b

theorem Relation.join_inr_reflTransGen {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} (r₂_ab : ReflTransGen r₂ a b) : ReflTransGen (r₁ ⊔ r₂) a b

theorem Relation.acyclic_le {α : Type u_1} {r s : α → α → Prop} (hle : r ≤ s) (ha : Acyclic s) : Acyclic r