principal_eq_map_coe_top — Mathlib

English

For any set s, the principal filter on s equals the push-forward of the top filter by the inclusion map: 𝓟 s = map ((↑) : s → α) ⊤.

Русский

Для любого множества s чистый фильтр 𝓟 s равен образу верхнего фильтра по включающей функции: 𝓟 s = map (включение) ⊤.

LaTeX

$$$ 𝓟 s = \operatorname{map} (\mathrm{Subtype.val}) \top $$$

Lean4

theorem principal_eq_map_coe_top (s : Set α) : 𝓟 s = map ((↑) : s → α) ⊤ := by simp

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