iSup_inf_principal — Mathlib

English

Let s_i be a family of subsets. The supremum of the principal filters 𝓟(s_i) equals the principal filter of the union ⋃_i s_i.

Русский

Пусть {s_i} — семейство подмножеств. Верхняя грань главных фильтров 𝓟(s_i) равна 𝓟(⋃_i s_i).

LaTeX

$$$\\bigsqcup_i \\mathcal{P}(s_i) = \\mathcal{P}\\Bigl(\\bigcup_i s_i\\Bigr)$$$

Lean4

theorem iSup_inf_principal (f : ι → Filter α) (s : Set α) : ⨆ i, f i ⊓ 𝓟 s = (⨆ i, f i) ⊓ 𝓟 s :=
  by
  ext
  simp only [mem_iSup, mem_inf_principal]

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