coe_sInf — Mathlib

English

The underlying relation of the infimum of a family of RingCon objects equals the infimum of the underlying relations.

Русский

У подлежащего отношения наименьшего элемента семейства RingCon равен наименьшему элементу отношений-основ RingCon.

LaTeX

$$$$ \operatorname{coe}(\iInf f) = \bigwedge_i \operatorname{coe}(f(i)) $$$$

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. -/
@[simp, norm_cast]
theorem coe_sInf (S : Set (RingCon R)) : ⇑(sInf S) = sInf ((⇑) '' S) := by ext;
  simp only [sInf_image, iInf_apply, iInf_Prop_eq]; rfl

Похожие утверждения