lift'_pure

Mathlib.Order.Filter.Lift

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

English

For any a, (pure a).lift' h = principal(h({a})).

Русский

Для любого элемента a, (pure a).lift' h = principal(h({a})).

LaTeX

$$$ {a : \\alpha} (hh : Monotone h) : (\\text{pure } a).lift' h = \\mathcal{P}(h\\{a\\}) $$$

Lean4

theorem lift'_pure {a : α} (hh : Monotone h) : (pure a : Filter α).lift' h = 𝓟 (h { a }) := by
  rw [← principal_singleton, lift'_principal hh]

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

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

Разделы

Аффилиация

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