lift_top — Mathlib

English

For any g: Set α → Filter β, lifting the top filter along g yields the evaluation at univ: (⊤ : Filter α).lift g = g univ.

Русский

Переотбор верхнего фильтра по функции g даёт тот же результат, что и значение g на всём множестве: (⊤).lift g = g univ.

LaTeX

$$$(\\top : \\text{Filter } \\alpha).\\mathrm{lift}\\, g = g(\\mathrm{univ})$$$

Lean4

@[simp]
theorem lift_top (g : Set α → Filter β) : (⊤ : Filter α).lift g = g univ := by simp [Filter.lift]

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