lift_le

Mathlib.Order.Filter.Lift

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

← MathLib Explorer

English

If s ∈ f and g(s) ≤ h, then f.lift g ≤ h.

Русский

Если s ∈ f и g(s) ≤ h, то f.lift g ≤ h.

LaTeX

$$(\forall s, s \in f \Rightarrow g(s) \le h) \Rightarrow f.lift g \le h$$

Lean4

theorem lift_le {f : Filter α} {g : Set α → Filter β} {h : Filter β} {s : Set α} (hs : s ∈ f) (hg : g s ≤ h) :
    f.lift g ≤ h :=
  iInf₂_le_of_le s hs hg

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

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

Разделы

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

Аффилиация

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