sup_principal — Mathlib

English

Let s and t be subsets of α. The join (supremum) of the principal filters 𝓟(s) and 𝓟(t) is the principal filter of the union s ∪ t.

Русский

Пусть s и t — подмножества α. Объединение (верхняя граница) главных фильтров 𝓟(s) и 𝓟(t) есть 𝓟(s ∪ t).

LaTeX

$$$\\mathcal{P}(s) \\vee \\mathcal{P}(t) = \\mathcal{P}(s \\cup t)$$$

Lean4

@[simp]
theorem sup_principal {s t : Set α} : 𝓟 s ⊔ 𝓟 t = 𝓟 (s ∪ t) :=
  Filter.ext fun u => by simp only [union_subset_iff, mem_sup, mem_principal]

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