coe_iInf — Mathlib

English

The carrier of the indexed infimum equals the intersection of all carriers, i.e., ⨅ i, f(i) corresponds to ⋂ i, (f(i) : Set α).

Русский

Носитель индексированного Inf равен пересечению всех носителей: ⨅ i, f(i) несёт носитель ⋂ i, (f(i) : Set α).

LaTeX

$$$\bigwedge_{i} f(i) = \bigcap_i (f(i) : \mathrm{Set} \alpha)$$$

Lean4

@[simp, norm_cast]
theorem coe_iInf (f : ι → Sublattice α) : ⨅ i, f i = ⋂ i, (f i : Set α) := by simp [iInf]

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