lift'_bot

Mathlib.Order.Filter.Lift

URI: https://scilib.ai/kg/mathlib#Filter.lift'_bot

English

The bottom filter lifted along h equals the principal filter of h(∅).

Русский

Нижний фильтр, поднятый по h, равен принципиальному фильтру h(∅).

LaTeX

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

Lean4

theorem lift'_bot (hh : Monotone h) : (⊥ : Filter α).lift' h = 𝓟 (h ∅) := by rw [← principal_empty, lift'_principal hh]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru