English
The inductively defined smallest congruence containing a binary relation r equals the infimum of the set of congruences containing r.
Русский
Постоянная конгруэнция, содержащая бинарное отношение r, равна наименьшему инфимума множества конгруэнций, содержащих r.
LaTeX
$$$\\operatorname{conGen} r = \\mathrm{sInf} \\{s : Con M \\mid \\forall x,y, r x y \\rightarrow s x y\\}$$$
Lean4
/-- The inductively defined smallest congruence relation containing a binary relation `r` equals
the infimum of the set of congruence relations containing `r`. -/
@[to_additive addConGen_eq /-- The inductively defined smallest additive congruence relation
containing a binary relation `r` equals the infimum of the set of additive congruence relations
containing `r`. -/
]
theorem conGen_eq (r : M → M → Prop) : conGen r = sInf {s : Con M | ∀ x y, r x y → s x y} :=
le_antisymm
(le_sInf
(fun s hs x y (hxy : (conGen r) x y) =>
show s x y by
apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy
· exact fun x y h => hs x y h
· exact s.refl'
· exact fun _ => s.symm'
· exact fun _ _ => s.trans'
· exact fun _ _ => s.mul))
(sInf_le ConGen.Rel.of)
