lift'_top — Mathlib

English

For any mapping h from sets of α to sets of β, the lift of the top filter along h is the principal filter generated by h(univ).

Русский

Для произвольного отображения h от множеств α в множества β, применение операции lift' к верхнему фильтру вдоль h даёт принципиальный фильтр, порождённый множеством h(универсум).

LaTeX

$$$ (\\top : \\mathrm{Filter}\\,\\alpha).lift' h = \\mathcal{P}(h\\,\\mathrm{univ}) $$$

Lean4

@[simp]
theorem lift'_top (h : Set α → Set β) : (⊤ : Filter α).lift' h = 𝓟 (h univ) :=
  lift_top _

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