English
For a set s of equivalence relations on α, the infimum of s, viewed as a relation, is the infimum of the images of s under the forgetful map to binary relations.
Русский
Пусть s — множество эквивалентностей на α. Инфимума над s, рассматриваемого как отношение, равна инфимума изображения s под отображением забывания к бинарным отношениям.
LaTeX
$$$ \\bigl( \\mathrm{sInf}\\, s \\bigr)\\!\\uparrow = \\mathrm{sInf}\\bigl( \\{ r \\mid r \\text{ arises from some } E \\in s \\} \\bigr) $$$$
Lean4
/-- The underlying binary operation of the infimum of a set of equivalence relations
is the infimum of the set's image under the map to the underlying binary operation. -/
theorem sInf_def {s : Set (Setoid α)} : ⇑(sInf s) = sInf ((⇑) '' s) :=
by
ext
simp only [sInf_image, iInf_apply, iInf_Prop_eq]
rfl
