lift'_le

Mathlib.Order.Filter.Lift

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

English

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

Русский

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

LaTeX

$$$ (hs : s \\in f) (hg : 𝓟 (g s) \\le h) \\Rightarrow f.lift' g \\le h $$$

Lean4

theorem lift'_le {f : Filter α} {g : Set α → Set β} {h : Filter β} {s : Set α} (hs : s ∈ f) (hg : 𝓟 (g s) ≤ h) :
    f.lift' g ≤ h :=
  lift_le hs hg

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

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

Разделы

Аффилиация

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