Relation closures

This file defines the reflexive, symmetric, transitive, reflexive transitive and equivalence closures of relations and proves some basic results on them.

Note that this is about unbundled relations, that is terms of types of the form α → β → Prop. For the bundled version, see Rel.

Definitions

• Relation.ReflGen: Reflexive closure. ReflGen r relates everything r related, plus for all a it relates a with itself. So ReflGen r a b ↔ r a b ∨ a = b.
• Relation.SymmGen: Symmetric closure. This is also the comparability relation, such that SymmGen r a b means that either r a b or r b a (see Mathlib.Order.Comparable)
• Relation.TransGen: Transitive closure. TransGen r relates everything r related transitively. So TransGen r a b ↔ ∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b.
• Relation.ReflTransGen: Reflexive transitive closure. ReflTransGen r relates everything r related transitively, plus for all a it relates a with itself. So ReflTransGen r a b ↔ (∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b) ∨ a = b. It is the same as the reflexive closure of the transitive closure, or the transitive closure of the reflexive closure. In terms of rewriting systems, this means that a can be rewritten to b in a number of rewrites.
• Relation.EqvGen: Equivalence closure. EqvGen r relates everything ReflTransGen r relates, plus for all related pairs it relates them in the opposite order.
• Relation.Comp: Relation composition. We provide notation ∘r. For r : α → β → Prop and s : β → γ → Prop, r ∘r s relates a : α and c : γ iff there exists b : β that's related to both.
• Relation.Map: Image of a relation under a pair of maps. For r : α → β → Prop, f : α → γ, g : β → δ, Map r f g is the relation γ → δ → Prop relating f a and g b for all a, b related by r.
• Relation.Join: Join of a relation. For r : α → α → Prop, Join r a b ↔ ∃ c, r a c ∧ r b c. In terms of rewriting systems, this means that a and b can be rewritten to the same term.

@[deprecated refl (since := "2026-03-27")]

theorem Std.Refl.reflexive {α : Sort u_1} {r : α → α → Prop} [Refl r] (a : α) : r a a

Alias of refl.

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

theorem IsRefl.reflexive {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] (a : α) : r a a

Alias of refl.

theorem Std.Refl.rel_of_ne_imp {α : Sort u_1} {r : α → α → Prop} [Refl r] {x y : α} (hr : x ≠ y → r x y) : r x y

To show a reflexive relation r : α → α → Prop holds over x y : α, it suffices to show it holds when x ≠ y.

@[deprecated Std.Refl.rel_of_ne_imp (since := "2026-03-27")]

theorem Reflexive.rel_of_ne_imp {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] {x y : α} (hr : x ≠ y → r x y) : r x y

Alias of Std.Refl.rel_of_ne_imp.

---

To show a reflexive relation r : α → α → Prop holds over x y : α, it suffices to show it holds when x ≠ y.

theorem Std.Refl.ne_imp_iff {α : Sort u_1} {r : α → α → Prop} [Refl r] {x y : α} : x ≠ y → r x y ↔ r x y

If a reflexive relation r : α → α → Prop holds over x y : α, then it holds whether or not x ≠ y.

@[deprecated Std.Refl.ne_imp_iff (since := "2026-03-27")]

theorem Reflexive.ne_imp_iff {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] {x y : α} : x ≠ y → r x y ↔ r x y

Alias of Std.Refl.ne_imp_iff.

---

If a reflexive relation r : α → α → Prop holds over x y : α, then it holds whether or not x ≠ y.

@[deprecated Std.Refl.ne_imp_iff (since := "2026-03-27")]

theorem reflexive_ne_imp_iff {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] {x y : α} : x ≠ y → r x y ↔ r x y

Alias of Std.Refl.ne_imp_iff.

---

If a reflexive relation r : α → α → Prop holds over x y : α, then it holds whether or not x ≠ y.

theorem refl_iff_subrelation_eq {α : Sort u_1} {r : α → α → Prop} : Std.Refl r ↔ Subrelation Eq r

@[deprecated refl_iff_subrelation_eq (since := "2026-03-27")]

theorem reflexive_iff_subrelation_eq {α : Sort u_1} {r : α → α → Prop} : Std.Refl r ↔ Subrelation Eq r

Alias of refl_iff_subrelation_eq.

theorem irrefl_iff_subrelation_ne {α : Sort u_1} {r : α → α → Prop} : Std.Irrefl r ↔ Subrelation r Ne

@[deprecated irrefl_iff_subrelation_ne (since := "2026-02-12")]

theorem irreflexive_iff_subrelation_ne {α : Sort u_1} {r : α → α → Prop} : Std.Irrefl r ↔ Subrelation r Ne

Alias of irrefl_iff_subrelation_ne.

theorem Std.Symm.iff {α : Sort u_1} {r : α → α → Prop} [Symm r] (x y : α) : r x y ↔ r y x

@[deprecated Std.Symm.iff (since := "2026-06-10")]

theorem Symmetric.iff {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] (x y : α) : r x y ↔ r y x

Alias of Std.Symm.iff.

theorem Std.Symm.flip_eq {α : Sort u_1} {r : α → α → Prop} [Symm r] : flip r = r

@[deprecated Std.Symm.flip_eq (since := "2026-06-10")]

theorem Symmetric.flip_eq {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : flip r = r

Alias of Std.Symm.flip_eq.

theorem Std.Symm.swap_eq {α : Sort u_1} {r : α → α → Prop} [Symm r] : Function.swap r = r

@[deprecated Std.Symm.swap_eq (since := "2026-06-10")]

theorem Symmetric.swap_eq {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : Function.swap r = r

Alias of Std.Symm.swap_eq.

theorem flip_eq_iff {α : Sort u_1} {r : α → α → Prop} : flip r = r ↔ Std.Symm r

theorem swap_eq_iff {α : Sort u_1} {r : α → α → Prop} : Function.swap r = r ↔ Std.Symm r

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

@[deprecated Std.Refl.comap (since := "2026-03-27")]

theorem Reflexive.comap {α : Sort u_1} {β : Sort u_2} {r : β → β → Prop} [Std.Refl r] (f : α → β) : Std.Refl (Function.onFun r f)

Alias of Std.Refl.comap.

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

@[deprecated Std.Symm.comap (since := "2026-06-10")]

theorem Symmetric.comap {α : Sort u_1} {β : Sort u_2} {r : β → β → Prop} [Std.Symm r] (f : α → β) : Std.Symm (Function.onFun r f)

Alias of Std.Symm.comap.

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

@[deprecated IsTrans.comap (since := "2026-02-21")]

theorem Transitive.comap {α : Sort u_1} {β : Sort u_2} {r : β → β → Prop} [IsTrans β r] (f : α → β) : IsTrans α (Function.onFun r f)

Alias of IsTrans.comap.

instance IsEquiv.comap {α : Sort u_1} {β : Sort u_2} {r : β → β → Prop} [IsEquiv β r] (f : α → β) : IsEquiv α (Function.onFun r f)

theorem Equivalence.comap {α : Sort u_1} {β : Sort u_2} {r : β → β → Prop} (h : Equivalence r) (f : α → β) : Equivalence (Function.onFun r f)

def Relation.Comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (r : α → β → Prop) (p : β → γ → Prop) (a : α) (c : γ) : Prop

The composition of two relations, yielding a new relation. The result relates a term of α and a term of γ if there is an intermediate term of β related to both.

Equations

• Relation.Comp r p a c = ∃ (b : β), r a b ∧ p b c

@[simp]

theorem Relation.comp_eq_fun {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {r : α → β → Prop} (f : γ → β) : (Comp r fun (x1 : β) (x2 : γ) => x1 = f x2) = fun (x1 : α) (x2 : γ) => r x1 (f x2)

@[simp]

theorem Relation.comp_eq {α : Sort u_1} {β : Sort u_2} {r : α → β → Prop} : (Comp r fun (x1 x2 : β) => x1 = x2) = r

@[simp]

theorem Relation.fun_eq_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {r : α → β → Prop} (f : γ → α) : Comp (fun (x1 : γ) (x2 : α) => f x1 = x2) r = fun (x : γ) => r (f x)

@[simp]

theorem Relation.eq_comp {α : Sort u_1} {β : Sort u_2} {r : α → β → Prop} : Comp (fun (x1 x2 : α) => x1 = x2) r = r

@[simp]

theorem Relation.iff_comp {α : Sort u_1} {r : Prop → α → Prop} : Comp (fun (x1 x2 : Prop) => x1 ↔ x2) r = r

@[simp]

theorem Relation.comp_iff {α : Sort u_1} {r : α → Prop → Prop} : (Comp r fun (x1 x2 : Prop) => x1 ↔ x2) = r

theorem Relation.comp_assoc {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop} : Comp (Comp r p) q = Comp r (Comp p q)

theorem Relation.flip_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {r : α → β → Prop} {p : β → γ → Prop} : flip (Comp r p) = Comp (flip p) (flip r)

def Relation.Fibration {α : Sort u_1} {β : Sort u_2} (rα : α → α → Prop) (rβ : β → β → Prop) (f : α → β) : Prop

A function f : α → β is a fibration between the relation rα and rβ if for all a : α and b : β, whenever b : β and f a are related by rβ, b is the image of some a' : α under f, and a' and a are related by rα.

Equations

• Relation.Fibration rα rβ f = ∀ ⦃a : α⦄ ⦃b : β⦄, rβ b (f a) → ∃ (a' : α), rα a' a ∧ f a' = b

theorem Acc.of_fibration {α : Sort u_1} {β : Sort u_2} {rα : α → α → Prop} {rβ : β → β → Prop} (f : α → β) (fib : Relation.Fibration rα rβ f) {a : α} (ha : Acc rα a) : Acc rβ (f a)

If f : α → β is a fibration between relations rα and rβ, and a : α is accessible under rα, then f a is accessible under rβ.

theorem Acc.of_downward_closed {α : Sort u_1} {β : Sort u_2} {rβ : β → β → Prop} (f : α → β) (dc : ∀ {a : α} {b : β}, rβ b (f a) → ∃ (c : α), f c = b) (a : α) (ha : Acc (InvImage rβ f) a) : Acc rβ (f a)

def Relation.Map {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (r : α → β → Prop) (f : α → γ) (g : β → δ) : γ → δ → Prop

The map of a relation r through a pair of functions pushes the relation to the codomains of the functions. The resulting relation is defined by having pairs of terms related if they have preimages related by r.

Equations

• Relation.Map r f g c d = ∃ (a : α), ∃ (b : β), r a b ∧ f a = c ∧ g b = d

theorem Relation.map_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {r : α → β → Prop} {f : α → γ} {g : β → δ} {c : γ} {d : δ} : Relation.Map r f g c d ↔ ∃ (a : α), ∃ (b : β), r a b ∧ f a = c ∧ g b = d

@[simp]

theorem Relation.map_map {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {ε : Sort u_5} {ζ : Sort u_6} (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → ζ) : Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁)

@[simp]

theorem Relation.map_apply_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → γ} {g : β → δ} (hf : Function.Injective f) (hg : Function.Injective g) (r : α → β → Prop) (a : α) (b : β) : Relation.Map r f g (f a) (g b) ↔ r a b

@[simp]

theorem Relation.map_id_id {α : Sort u_1} {β : Sort u_2} (r : α → β → Prop) : Relation.Map r id id = r

@[implicit_reducible]

instance Relation.instDecidableMapOfExistsAndEq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {r : α → β → Prop} {f : α → γ} {g : β → δ} {c : γ} {d : δ} [Decidable (∃ (a : α), ∃ (b : β), r a b ∧ f a = c ∧ g b = d)] : Decidable (Relation.Map r f g c d)

Equations

• Relation.instDecidableMapOfExistsAndEq = inst✝

theorem Std.Refl.map {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} [Refl r] {f : α → β} (hf : Function.Surjective f) : Refl (Relation.Map r f f)

@[deprecated Std.Refl.map (since := "2026-03-27")]

theorem Relation.map_reflexive {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} [Std.Refl r] {f : α → β} (hf : Function.Surjective f) : Std.Refl (Relation.Map r f f)

Alias of Std.Refl.map.

instance Std.Symm.map {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} [Symm r] (f : α → β) : Symm (Relation.Map r f f)

@[deprecated Std.Symm.map (since := "2026-06-10")]

theorem Relation.map_symmetric {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} [Std.Symm r] (f : α → β) : Std.Symm (Relation.Map r f f)

Alias of Std.Symm.map.

theorem IsTrans.map {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} [IsTrans α r] {f : α → β} (hf : ∀ (x y : α), f x = f y → r x y) : IsTrans β (Relation.Map r f f)

@[deprecated IsTrans.map (since := "2026-03-27")]

theorem Relation.isTrans_map {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} [IsTrans α r] {f : α → β} (hf : ∀ (x y : α), f x = f y → r x y) : IsTrans β (Relation.Map r f f)

Alias of IsTrans.map.

@[deprecated Relation.isTrans_map (since := "2026-02-21")]

theorem Relation.map_transitive {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} [IsTrans α r] {f : α → β} (hf : ∀ (x y : α), f x = f y → r x y) : IsTrans β (Relation.Map r f f)

Alias of Relation.isTrans_map.

---

Alias of IsTrans.map.

theorem Relation.map_equivalence {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} (hr : Equivalence r) (f : α → β) (hf : Function.Surjective f) (hf_ker : ∀ (x y : α), f x = f y → r x y) : Equivalence (Relation.Map r f f)

theorem Relation.map_mono {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {r s : α → β → Prop} {f : α → γ} {g : β → δ} (h : ∀ (x : α) (y : β), r x y → s x y) (x : γ) (y : δ) : Relation.Map r f g x y → Relation.Map s f g x y

theorem Relation.le_onFun_map {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} (f : α → β) : Subrelation r (Function.onFun (Relation.Map r f f) f)

theorem Relation.onFun_map_eq_of_injective {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {f : α → β} (hinj : Function.Injective f) : Function.onFun (Relation.Map r f f) f = r

theorem Relation.map_onFun_le {α : Sort u_1} {β : Sort u_2} {r : β → β → Prop} (f : α → β) : Subrelation (Relation.Map (Function.onFun r f) f f) r

theorem Relation.map_onFun_eq_of_surjective {α : Sort u_1} {β : Sort u_2} {r : β → β → Prop} {f : α → β} (hsurj : Function.Surjective f) : Relation.Map (Function.onFun r f) f f = r

theorem Relation.map_onFun_map_eq_map {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} (f : α → β) : Relation.Map (Function.onFun (Relation.Map r f f) f) f f = Relation.Map r f f

theorem Relation.onFun_map_onFun_eq_onFun {α : Sort u_1} {β : Sort u_2} {r : β → β → Prop} (f : α → β) : Function.onFun (Relation.Map (Function.onFun r f) f f) f = Function.onFun r f

theorem Relation.onFun_map_onFun_iff_onFun {α : Sort u_1} {β : Sort u_2} {r : β → β → Prop} (f : α → β) (a₁ a₂ : α) : Relation.Map (Function.onFun r f) f f (f a₁) (f a₂) ↔ r (f a₁) (f a₂)

inductive Relation.ReflTransGen {α : Sort u_1} (r : α → α → Prop) (a : α) : α → Prop

ReflTransGen r: reflexive transitive closure of r

• refl {α : Sort u_1} {r : α → α → Prop} {a : α} : ReflTransGen r a a
• tail {α : Sort u_1} {r : α → α → Prop} {a b c : α} : ReflTransGen r a b → r b c → ReflTransGen r a c

theorem Relation.ReflTransGen.cases_tail_iff {α : Sort u_1} (r : α → α → Prop) (a a✝ : α) : ReflTransGen r a a✝ ↔ a✝ = a ∨ ∃ (b : α), ReflTransGen r a b ∧ r b a✝

inductive Relation.ReflGen {α : Sort u_1} (r : α → α → Prop) (a : α) : α → Prop

ReflGen r: reflexive closure of r

• refl {α : Sort u_1} {r : α → α → Prop} {a : α} : ReflGen r a a
• single {α : Sort u_1} {r : α → α → Prop} {a b : α} : r a b → ReflGen r a b

theorem Relation.reflGen_iff {α : Sort u_1} (r : α → α → Prop) (a a✝ : α) : ReflGen r a a✝ ↔ a✝ = a ∨ r a a✝

def Relation.SymmGen {α : Sort u_1} (r : α → α → Prop) (a b : α) : Prop

SymmGen r: symmetric closure of r. This is also the comparability relation, such that SymmGen r a b means that either r a b or r b a (see Mathlib.Order.Comparable).

Equations

• Relation.SymmGen r a b = (r a b ∨ r b a)

inductive Relation.EqvGen {α : Sort u_1} (r : α → α → Prop) : α → α → Prop

EqvGen r: equivalence closure of r.

• rel {α : Sort u_1} {r : α → α → Prop} (x y : α) : r x y → EqvGen r x y
• refl {α : Sort u_1} {r : α → α → Prop} (x : α) : EqvGen r x x
• symm {α : Sort u_1} {r : α → α → Prop} (x y : α) : EqvGen r x y → EqvGen r y x
• trans {α : Sort u_1} {r : α → α → Prop} (x y z : α) : EqvGen r x y → EqvGen r y z → EqvGen r x z

theorem Relation.eqvGen_iff {α : Sort u_1} (r : α → α → Prop) (a✝ a✝¹ : α) : EqvGen r a✝ a✝¹ ↔ r a✝ a✝¹ ∨ a✝¹ = a✝ ∨ EqvGen r a✝¹ a✝ ∨ ∃ (y : α), EqvGen r a✝ y ∧ EqvGen r y a✝¹

theorem Relation.transGen_iff {α : Sort u} (r : α → α → Prop) (a✝ a✝¹ : α) : TransGen r a✝ a✝¹ ↔ r a✝ a✝¹ ∨ ∃ (b : α), TransGen r a✝ b ∧ r b a✝¹

theorem Relation.ReflGen.to_reflTransGen {α : Sort u_1} {r : α → α → Prop} {a b : α} : ReflGen r a b → ReflTransGen r a b

theorem Relation.ReflGen.mono {α : Sort u_1} {r p : α → α → Prop} (hp : ∀ (a b : α), r a b → p a b) {a b : α} : ReflGen r a b → ReflGen p a b

instance Relation.ReflGen.instRefl {α : Sort u_1} {r : α → α → Prop} : Std.Refl (ReflGen r)

instance Relation.ReflGen.stdSymm {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : Std.Symm (ReflGen r)

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

theorem Relation.ReflGen.symmetric {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : Std.Symm (ReflGen r)

Alias of Relation.ReflGen.stdSymm.

instance Relation.ReflGen.instIsTrans {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] : IsTrans α (ReflGen r)

theorem Relation.SymmGen.of_rel {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : r a b) : SymmGen r a b

theorem Relation.SymmGen.of_rel_symm {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : r b a) : SymmGen r a b

theorem Relation.SymmGen.swap {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : SymmGen r b a) : SymmGen (Function.swap r) a b

@[simp]

theorem Relation.SymmGen.refl {α : Sort u_1} (r : α → α → Prop) [Std.Refl r] (a : α) : SymmGen r a a

theorem Relation.SymmGen.rfl {α : Sort u_1} {r : α → α → Prop} {a : α} [Std.Refl r] : SymmGen r a a

instance Relation.SymmGen.instRefl {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] : Std.Refl (SymmGen r)

theorem Relation.SymmGen.symm {α : Sort u_1} {r : α → α → Prop} {a b : α} : SymmGen r a b → SymmGen r b a

instance Relation.SymmGen.instSymm {α : Sort u_1} {r : α → α → Prop} : Std.Symm (SymmGen r)

@[implicit_reducible]

instance Relation.SymmGen.decidableRel {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] : DecidableRel (SymmGen r)

Equations

• Relation.SymmGen.decidableRel x✝¹ x✝ = Relation.SymmGen.decidableRel._aux_1 x✝¹ x✝

theorem Relation.SymmGen.of_le {α : Type u_7} [LE α] {a b : α} (h : a ≤ b) : SymmGen (fun (x1 x2 : α) => x1 ≤ x2) a b

theorem Relation.SymmGen.of_ge {α : Type u_7} [LE α] {a b : α} (h : b ≤ a) : SymmGen (fun (x1 x2 : α) => x1 ≤ x2) a b

theorem LE.le.symmGen {α : Type u_7} [LE α] {a b : α} (h : a ≤ b) : Relation.SymmGen (fun (x1 x2 : α) => x1 ≤ x2) a b

Alias of Relation.SymmGen.of_le.

theorem LE.le.symmGen_symm {α : Type u_7} [LE α] {a b : α} (h : b ≤ a) : Relation.SymmGen (fun (x1 x2 : α) => x1 ≤ x2) a b

Alias of Relation.SymmGen.of_ge.

theorem Relation.ReflTransGen.trans {α : Sort u_1} {r : α → α → Prop} {a b c : α} (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c

theorem Relation.ReflTransGen.single {α : Sort u_1} {r : α → α → Prop} {a b : α} (hab : r a b) : ReflTransGen r a b

theorem Relation.ReflTransGen.head {α : Sort u_1} {r : α → α → Prop} {a b c : α} (hab : r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c

instance Relation.ReflTransGen.stdSymm {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : Std.Symm (ReflTransGen r)

@[deprecated Relation.ReflTransGen.stdSymm (since := "2026-06-10")]

theorem Relation.ReflTransGen.symmetric {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : Std.Symm (ReflTransGen r)

Alias of Relation.ReflTransGen.stdSymm.

theorem Relation.ReflTransGen.cases_tail {α : Sort u_1} {r : α → α → Prop} {a b : α} : ReflTransGen r a b → b = a ∨ ∃ (c : α), ReflTransGen r a c ∧ r c b

theorem Relation.ReflTransGen.head_induction_on {α : Sort u_1} {r : α → α → Prop} {b : α} {motive : (a : α) → ReflTransGen r a b → Prop} {a : α} (h : ReflTransGen r a b) (refl : motive b ⋯) (head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯) : motive a h

theorem Relation.ReflTransGen.trans_induction_on {α : Sort u_1} {r : α → α → Prop} {motive : {a b : α} → ReflTransGen r a b → Prop} {a b : α} (h : ReflTransGen r a b) (refl : ∀ (a : α), motive ⋯) (single : ∀ {a b : α} (h : r a b), motive ⋯) (trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯) : motive h

theorem Relation.ReflTransGen.cases_head {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : ReflTransGen r a b) : a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b

theorem Relation.ReflTransGen.cases_head_iff {α : Sort u_1} {r : α → α → Prop} {a b : α} : ReflTransGen r a b ↔ a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b

theorem Relation.ReflTransGen.total_of_right_unique {α : Sort u_1} {r : α → α → Prop} {a b c : α} (U : Relator.RightUnique r) (ab : ReflTransGen r a b) (ac : ReflTransGen r a c) : ReflTransGen r b c ∨ ReflTransGen r c b

theorem Relation.TransGen.to_reflTransGen {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : TransGen r a b) : ReflTransGen r a b

theorem Relation.TransGen.trans_left {α : Sort u_1} {r : α → α → Prop} {a b c : α} (hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c

theorem Relation.TransGen.head' {α : Sort u_1} {r : α → α → Prop} {a b c : α} (hab : r a b) (hbc : ReflTransGen r b c) : TransGen r a c

theorem Relation.TransGen.tail' {α : Sort u_1} {r : α → α → Prop} {a b c : α} (hab : ReflTransGen r a b) (hbc : r b c) : TransGen r a c

theorem Relation.TransGen.head {α : Sort u_1} {r : α → α → Prop} {a b c : α} (hab : r a b) (hbc : TransGen r b c) : TransGen r a c

theorem Relation.TransGen.head_induction_on {α : Sort u_1} {r : α → α → Prop} {b : α} {motive : (a : α) → TransGen r a b → Prop} {a : α} (h : TransGen r a b) (single : ∀ {a : α} (h : r a b), motive a ⋯) (head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯) : motive a h

theorem Relation.TransGen.trans_induction_on {α : Sort u_1} {r : α → α → Prop} {motive : {a b : α} → TransGen r a b → Prop} {a b : α} (h : TransGen r a b) (single : ∀ {a b : α} (h : r a b), motive ⋯) (trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯) : motive h

theorem Relation.TransGen.trans_right {α : Sort u_1} {r : α → α → Prop} {a b c : α} (hab : ReflTransGen r a b) (hbc : TransGen r b c) : TransGen r a c

theorem Relation.TransGen.tail'_iff {α : Sort u_1} {r : α → α → Prop} {a c : α} : TransGen r a c ↔ ∃ (b : α), ReflTransGen r a b ∧ r b c

theorem Relation.TransGen.head'_iff {α : Sort u_1} {r : α → α → Prop} {a c : α} : TransGen r a c ↔ ∃ (b : α), r a b ∧ ReflTransGen r b c

instance Relation.TransGen.stdSymm {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : Std.Symm (TransGen r)

@[deprecated Relation.TransGen.stdSymm (since := "2026-06-10")]

theorem Relation.TransGen.symmetric {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] : Std.Symm (TransGen r)

Alias of Relation.TransGen.stdSymm.

instance Relation.TransGen.instRefl_mathlib {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] : Std.Refl (TransGen r)

theorem Relation.reflGen_eq_self {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] : ReflGen r = r

@[deprecated inferInstance (since := "2026-03-27")]

theorem Relation.reflexive_reflGen {α : Sort u_1} {r : α → α → Prop} : Std.Refl (ReflGen r)

theorem Relation.reflGen_minimal {α : Sort u_1} {r r' : α → α → Prop} [Std.Refl r'] (h : ∀ (x y : α), r x y → r' x y) {x y : α} (hxy : ReflGen r x y) : r' x y

theorem Relation.symmGen_swap {α : Sort u_1} (r : α → α → Prop) : SymmGen (Function.swap r) = SymmGen r

theorem Relation.symmGen_swap_apply {α : Sort u_1} {a b : α} (r : α → α → Prop) : SymmGen (Function.swap r) a b ↔ SymmGen r a b

theorem Relation.symmGen_comm {α : Sort u_1} {r : α → α → Prop} {a b : α} : SymmGen r a b ↔ SymmGen r b a

@[simp]

theorem Relation.symmGen_of_total {α : Sort u_1} {r : α → α → Prop} [Std.Total r] (a b : α) : SymmGen r a b

instance Relation.instIsTransTransGen {α : Sort u_1} {r : α → α → Prop} : IsTrans α (TransGen r)

@[implicit_reducible]

instance Relation.instTransTransGen_mathlib {α : Sort u_1} {r : α → α → Prop} : Trans (TransGen r) r (TransGen r)

Equations

• Relation.instTransTransGen_mathlib = { trans := ⋯ }

@[implicit_reducible]

instance Relation.instTransTransGen_mathlib_1 {α : Sort u_1} {r : α → α → Prop} : Trans r (TransGen r) (TransGen r)

Equations

• Relation.instTransTransGen_mathlib_1 = { trans := ⋯ }

@[implicit_reducible]

instance Relation.instTransTransGenReflTransGen {α : Sort u_1} {r : α → α → Prop} : Trans (TransGen r) (ReflTransGen r) (TransGen r)

Equations

• Relation.instTransTransGenReflTransGen = { trans := ⋯ }

@[implicit_reducible]

instance Relation.instTransReflTransGenTransGen {α : Sort u_1} {r : α → α → Prop} : Trans (ReflTransGen r) (TransGen r) (TransGen r)

Equations

• Relation.instTransReflTransGenTransGen = { trans := ⋯ }

theorem Relation.transGen_eq_self {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] : TransGen r = r

@[deprecated inferInstance (since := "2026-02-21")]

theorem Relation.transitive_transGen {α : Sort u_1} {r : α → α → Prop} : IsTrans α (TransGen r)

@[deprecated Relation.transGen_eq_self (since := "2026-03-27")]

theorem Relation.transGen_idem {α : Sort u_1} {r : α → α → Prop} : TransGen (TransGen r) = TransGen r

theorem Relation.TransGen.lift {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ (a b : α), r a b → p (f a) (f b)) (hab : TransGen r a b) : TransGen p (f a) (f b)

theorem Relation.TransGen.lift' {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ (a b : α), r a b → TransGen p (f a) (f b)) (hab : TransGen r a b) : TransGen p (f a) (f b)

theorem Relation.TransGen.closed {α : Sort u_1} {r : α → α → Prop} {a b : α} {p : α → α → Prop} : (∀ (a b : α), r a b → TransGen p a b) → TransGen r a b → TransGen p a b

theorem Relation.TransGen.closed' {α : Sort u_1} {r : α → α → Prop} {P : α → Prop} (dc : ∀ {a b : α}, r a b → P b → P a) {a b : α} (h : TransGen r a b) : P b → P a

theorem Relation.TransGen.mono {α : Sort u_1} {r : α → α → Prop} {a b : α} {p : α → α → Prop} : (∀ (a b : α), r a b → p a b) → TransGen r a b → TransGen p a b

theorem Relation.transGen_minimal {α : Sort u_1} {r r' : α → α → Prop} [IsTrans α r'] (h : ∀ (x y : α), r x y → r' x y) {x y : α} (hxy : TransGen r x y) : r' x y

theorem Relation.TransGen.swap {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : TransGen r b a) : TransGen (Function.swap r) a b

theorem Relation.transGen_swap {α : Sort u_1} {r : α → α → Prop} {a b : α} : TransGen (Function.swap r) a b ↔ TransGen r b a

theorem Relation.reflTransGen_iff_eq {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : ∀ (b : α), ¬r a b) : ReflTransGen r a b ↔ b = a

theorem Relation.reflTransGen_iff_eq_or_transGen {α : Sort u_1} {r : α → α → Prop} {a b : α} : ReflTransGen r a b ↔ b = a ∨ TransGen r a b

theorem Relation.ReflTransGen.lift {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ (a b : α), r a b → p (f a) (f b)) (hab : ReflTransGen r a b) : ReflTransGen p (f a) (f b)

theorem Relation.ReflTransGen.mono {α : Sort u_1} {r : α → α → Prop} {a b : α} {p : α → α → Prop} : (∀ (a b : α), r a b → p a b) → ReflTransGen r a b → ReflTransGen p a b

theorem Relation.reflTransGen_eq_self {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] [IsTrans α r] : ReflTransGen r = r

@[implicit_reducible]

instance Relation.instTransReflTransGen {α : Sort u_1} {r : α → α → Prop} : Trans r (ReflTransGen r) (ReflTransGen r)

Equations

• Relation.instTransReflTransGen = { trans := ⋯ }

@[implicit_reducible]

instance Relation.instTransReflTransGen_1 {α : Sort u_1} {r : α → α → Prop} : Trans (ReflTransGen r) r (ReflTransGen r)

Equations

• Relation.instTransReflTransGen_1 = { trans := ⋯ }

instance Relation.instReflReflTransGen {α : Sort u_1} {r : α → α → Prop} : Std.Refl (ReflTransGen r)

@[deprecated inferInstance (since := "2026-03-27")]

theorem Relation.reflexive_reflTransGen {α : Sort u_1} {r : α → α → Prop} : Std.Refl (ReflTransGen r)

instance Relation.instIsTransReflTransGen {α : Sort u_1} {r : α → α → Prop} : IsTrans α (ReflTransGen r)

@[deprecated inferInstance (since := "2026-02-21")]

theorem Relation.transitive_reflTransGen {α : Sort u_1} {r : α → α → Prop} : IsTrans α (ReflTransGen r)

@[deprecated Relation.reflTransGen_eq_self (since := "2026-03-27")]

theorem Relation.reflTransGen_idem {α : Sort u_1} {r : α → α → Prop} : ReflTransGen (ReflTransGen r) = ReflTransGen r

theorem Relation.ReflTransGen.lift' {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ (a b : α), r a b → ReflTransGen p (f a) (f b)) (hab : ReflTransGen r a b) : ReflTransGen p (f a) (f b)

theorem Relation.reflTransGen_closed {α : Sort u_1} {r : α → α → Prop} {a b : α} {p : α → α → Prop} : (∀ (a b : α), r a b → ReflTransGen p a b) → ReflTransGen r a b → ReflTransGen p a b

theorem Relation.ReflTransGen.swap {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : ReflTransGen r b a) : ReflTransGen (Function.swap r) a b

theorem Relation.reflTransGen_swap {α : Sort u_1} {r : α → α → Prop} {a b : α} : ReflTransGen (Function.swap r) a b ↔ ReflTransGen r b a

@[simp]

theorem Relation.reflGen_transGen {α : Sort u_1} {r : α → α → Prop} : ReflGen (TransGen r) = ReflTransGen r

@[simp]

theorem Relation.transGen_reflGen {α : Sort u_1} {r : α → α → Prop} : TransGen (ReflGen r) = ReflTransGen r

@[simp]

theorem Relation.reflTransGen_reflGen {α : Sort u_1} {r : α → α → Prop} : ReflTransGen (ReflGen r) = ReflTransGen r

@[simp]

theorem Relation.reflTransGen_transGen {α : Sort u_1} {r : α → α → Prop} : ReflTransGen (TransGen r) = ReflTransGen r

theorem Relation.reflTransGen_eq_transGen {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] : ReflTransGen r = TransGen r

theorem Relation.reflTransGen_eq_reflGen {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] : ReflTransGen r = ReflGen r

theorem Relation.EqvGen.is_equivalence {α : Sort u_1} (r : α → α → Prop) : Equivalence (EqvGen r)

@[implicit_reducible]

def Relation.EqvGen.setoid {α : Sort u_1} (r : α → α → Prop) : Setoid α

EqvGen.setoid r is the setoid generated by a relation r.

The motivation for this definition is that Quot r behaves like Quotient (EqvGen.setoid r), see for example Quot.eqvGen_exact and Quot.eqvGen_sound.

Equations

• Relation.EqvGen.setoid r = { r := Relation.EqvGen r, iseqv := ⋯ }

theorem Relation.EqvGen.mono {α : Sort u_1} {a b : α} {r p : α → α → Prop} (hrp : ∀ (a b : α), r a b → p a b) (h : EqvGen r a b) : EqvGen p a b

def Relation.Join {α : Sort u_1} (r : α → α → Prop) : α → α → Prop

The join of a relation on a single type is a new relation for which pairs of terms are related if there is a third term they are both related to. For example, if r is a relation representing rewrites in a term rewriting system, then confluence is the property that if a rewrites to both b and c, then join r relates b and c (see Relation.church_rosser).

Equations

• Relation.Join r a b = ∃ (c : α), r a c ∧ r b c

theorem Relation.church_rosser {α : Sort u_1} {r : α → α → Prop} {a b c : α} (h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d) (hab : ReflTransGen r a b) (hac : ReflTransGen r a c) : Join (ReflTransGen r) b c

A sufficient condition for the Church-Rosser property.

theorem Relation.join_of_single {α : Sort u_1} {r : α → α → Prop} {a b : α} [Std.Refl r] (hab : r a b) : Join r a b

instance Relation.Join.symm {α : Sort u_1} {r : α → α → Prop} : Std.Symm (Join r)

@[deprecated Relation.Join.symm (since := "2026-06-10")]

theorem Relation.symmetric_join {α : Sort u_1} {r : α → α → Prop} : Std.Symm (Join r)

Alias of Relation.Join.symm.

instance Relation.Join.refl {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] : Std.Refl (Join r)

@[deprecated Relation.Join.refl (since := "2026-06-10")]

theorem Relation.reflexive_join {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] : Std.Refl (Join r)

Alias of Relation.Join.refl.

theorem Relation.isTrans_join {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] (h : ∀ (a b c : α), r a b → r a c → Join r b c) : IsTrans α (Join r)

@[deprecated Relation.isTrans_join (since := "2026-02-21")]

theorem Relation.transitive_join {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] (h : ∀ (a b c : α), r a b → r a c → Join r b c) : IsTrans α (Join r)

Alias of Relation.isTrans_join.

theorem Relation.equivalence_join {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] [IsTrans α r] (h : ∀ (a b c : α), r a b → r a c → Join r b c) : Equivalence (Join r)

theorem Relation.equivalence_join_reflTransGen {α : Sort u_1} {r : α → α → Prop} (h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d) : Equivalence (Join (ReflTransGen r))

theorem Relation.join_of_equivalence {α : Sort u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} (hr : Equivalence r) (h : ∀ (a b : α), r' a b → r a b) : Join r' a b → r a b

theorem Relation.reflTransGen_of_isTrans_reflexive {α : Sort u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} [Std.Refl r] [IsTrans α r] (h : ∀ (a b : α), r' a b → r a b) (h' : ReflTransGen r' a b) : r a b

@[deprecated Relation.reflTransGen_of_isTrans_reflexive (since := "2026-02-21")]

theorem Relation.reflTransGen_of_transitive_reflexive {α : Sort u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} [Std.Refl r] [IsTrans α r] (h : ∀ (a b : α), r' a b → r a b) (h' : ReflTransGen r' a b) : r a b

Alias of Relation.reflTransGen_of_isTrans_reflexive.

@[deprecated Relation.reflTransGen_of_transitive_reflexive (since := "2025-12-17")]

theorem Relation.reflTransGen_minimal {α : Sort u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} [Std.Refl r] [IsTrans α r] (h : ∀ (a b : α), r' a b → r a b) (h' : ReflTransGen r' a b) : r a b

Alias of Relation.reflTransGen_of_transitive_reflexive.

---

Alias of Relation.reflTransGen_of_isTrans_reflexive.

theorem Relation.reflTransGen_of_equivalence {α : Sort u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} (hr : Equivalence r) : (∀ (a b : α), r' a b → r a b) → ReflTransGen r' a b → r a b

theorem Quot.eqvGen_exact {α : Sort u_1} {r : α → α → Prop} {a b : α} (H : mk r a = mk r b) : Relation.EqvGen r a b

theorem Quot.eqvGen_sound {α : Sort u_1} {r : α → α → Prop} {a b : α} (H : Relation.EqvGen r a b) : mk r a = mk r b

theorem Equivalence.eqvGen_iff {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : Equivalence r) : Relation.EqvGen r a b ↔ r a b

theorem Equivalence.eqvGen_eq {α : Sort u_1} {r : α → α → Prop} (h : Equivalence r) : Relation.EqvGen r = r