le_lift

Mathlib.Order.Filter.Lift

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

English

The inequality h ≤ f.lift g holds exactly when ∀ s ∈ f, h ≤ g(s).

Русский

Неравенство h ≤ f.lift g эквивалентно ∀ s ∈ f, h ≤ g(s).

LaTeX

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

Lean4

theorem le_lift {f : Filter α} {g : Set α → Filter β} {h : Filter β} : h ≤ f.lift g ↔ ∀ s ∈ f, h ≤ g s :=
  le_iInf₂_iff

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

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

Разделы

Аффилиация

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