iInf_def — Mathlib

English

If you take a family S(i) of subsets with closedness preserved, the infimum of the corresponding closed sets equals the closed set with carrier ⋂ i S(i) and the appropriate closedness proof.

Русский

Если взять семейство множеств S(i) с сохранившейся замкнутостью и взять соответствующие замкнутые множества, то infimum равен замкнутому множеству с носителем ⋂ i S(i) и соответствующим доказательством замкнутости.

LaTeX

$$$\bigwedge_i \langle S(i), h(i)\rangle = \langle \bigcap_i S(i), \text{isClosed_iInter}(h)\rangle.$$$

Lean4

theorem iInf_def {ι} (s : ι → Closeds α) : ⨅ i, s i = ⟨⋂ i, s i, isClosed_iInter fun i => (s i).2⟩ := by ext1; simp

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