eqvGen_eq — Mathlib

English

The equivalence closure of an equivalence relation r is r itself.

Русский

Замыкание по эквивалентности для равного отношения r возвращает само r.

LaTeX

$$$$ EqvGen.setoid r.r = r. $$$$

Lean4

/-- The inductively defined equivalence closure of a binary relation r is the infimum
of the set of all equivalence relations containing r. -/
theorem eqvGen_eq (r : α → α → Prop) : EqvGen.setoid r = sInf {s : Setoid α | ∀ ⦃x y⦄, r x y → s x y} :=
  le_antisymm
    (fun _ _ H => EqvGen.rec (fun _ _ h _ hs => hs h) (refl' _) (fun _ _ _ => symm' _) (fun _ _ _ _ _ => trans' _) H)
    (sInf_le fun _ _ h => EqvGen.rel _ _ h)

Похожие утверждения