iSup_principal — Mathlib

English

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

Русский

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

LaTeX

$$$\\bigvee_{i} \\mathcal{P}(s_i) = \\mathcal{P}\\Bigl(\\bigcup_{i} s_i\\Bigr)$$$

Lean4

@[simp]
theorem iSup_principal {ι : Sort w} {s : ι → Set α} : ⨆ x, 𝓟 (s x) = 𝓟 (⋃ i, s i) :=
  Filter.ext fun x => by simp only [mem_iSup, mem_principal, iUnion_subset_iff]

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