lift_principal

Mathlib.Order.Filter.Lift

URI: https://scilib.ai/kg/mathlib#Filter.lift_principal

← MathLib Explorer

English

A principal filter lifts to the original filter: (𝓟 s).lift g = g(s).

Русский

У фильтра-принципа подъём равен g(s).

LaTeX

$$(\mathcal{P} s) . lift g = g s$$

Lean4

theorem lift_principal {s : Set α} (hg : Monotone g) : (𝓟 s).lift g = g s :=
  (lift_le (mem_principal_self _) le_rfl).antisymm (le_lift.2 fun _t ht => hg ht)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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