English
The smallest congruence containing r equals the infimum of all congruences containing r.
Русский
Наименьшее конгруэнтное отношение, содержащее r, равно наименьшему из всех конгруэнтных отношений, содержащих r.
LaTeX
$$$$ \operatorname{ringConGen}(r) = \inf\{ s : RingCon(R) \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`. -/
theorem ringConGen_eq (r : R → R → Prop) : ringConGen r = sInf {s : RingCon R | ∀ x y, r x y → s x y} :=
le_antisymm
(fun _x _y H =>
RingConGen.Rel.recOn H (fun _ _ h _ hs => hs _ _ h) (RingCon.refl _) (fun _ => RingCon.symm _)
(fun _ _ => RingCon.trans _) (fun _ _ h1 h2 c hc => c.add (h1 c hc) <| h2 c hc)
(fun _ _ h1 h2 c hc => c.mul (h1 c hc) <| h2 c hc))
(sInf_le fun _ _ => RingConGen.Rel.of _ _)
