English
The infimum of a set of congruences equals the infimum of their image under the map to the underlying Setoid.
Русский
Нижнее предел множества конгруэнций равен нижнему пределу образа этого множества под отображением к базовому Setoid.
LaTeX
$$$\\text{Infimum}(S)\\toSetoid = \\text{Infimum}(\\text{toSetoid}''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 equivalence relation. -/
@[to_additive /-- 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 equivalence relation. -/
]
theorem sInf_toSetoid (S : Set (Con M)) : (sInf S).toSetoid = sInf (toSetoid '' S) :=
Setoid.ext fun x y => ⟨fun h r ⟨c, hS, hr⟩ => by rw [← hr]; exact h c hS, fun h c hS => h c.toSetoid ⟨c, hS, rfl⟩⟩
