inf_principal — Mathlib

English

Let s and t be subsets of α. The meet (infimum) of the principal filters 𝓟(s) and 𝓟(t) is the principal filter of the intersection s ∩ t.

Русский

Пусть s и t — подмножества множества α. Наименьшее верхнее пределовое (пересечение) главных фильтров 𝓟(s) и 𝓟(t) есть главный фильтр над множестом s ∩ t.

LaTeX

$$$\\mathcal{P}(s) \\sqcap \\mathcal{P}(t) = \\mathcal{P}(s \\cap t)$$$

Lean4

@[simp]
theorem inf_principal {s t : Set α} : 𝓟 s ⊓ 𝓟 t = 𝓟 (s ∩ t) :=
  le_antisymm (by simp only [le_principal_iff, mem_inf_iff]; exact ⟨s, Subset.rfl, t, Subset.rfl, rfl⟩)
    (by simp [le_inf_iff, inter_subset_left, inter_subset_right])

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