English
The infimum of a set of congruences, when coerced to relations, equals the infimum of the image under the coercion map.
Русский
Предел множества конгруэнций, приведенный к отношениям, равен пределу образа под отображением коэфа.
LaTeX
$$$\\uparrow (\\mathrm{sInf}\\;S) = \\mathrm{sInf}\\; (\\uparrow)''S$$$
Lean4
/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
under the map to the underlying binary relation. -/
@[to_additive (attr := simp, norm_cast) /--
The infimum of a set of additive congruence relations is the same as the infimum
of the set's image under the map to the underlying binary relation. -/
]
theorem coe_sInf (S : Set (Con M)) : ⇑(sInf S) = sInf ((⇑) '' S) :=
by
ext
simp only [sInf_image, iInf_apply, iInf_Prop_eq]
rfl
