coe_iInf — Mathlib

English

The infimum of a family of closed sets is the closed set whose carrier is the intersection of the carriers, together with the closedness proof that the intersection is closed.

Русский

Infimum семейства замкнутых множеств — это замкнутое множество с носителем равным пересечению носителей и с доказательством того, что пересечение замкнуто.

LaTeX

$$$\bigwedge_i s(i) = \langle \bigcap_i s(i), \text{isClosed_iInter}(i \mapsto s(i).2)\rangle.$$$

Lean4

@[simp, norm_cast]
theorem coe_iInf {ι} (s : ι → Closeds α) : ((⨅ i, s i : Closeds α) : Set α) = ⋂ i, s i := by ext; simp

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