lift_mono'

Mathlib.Order.Filter.Lift

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

English

If ∀ s ∈ f, g1(s) ≤ g2(s) then f.lift g1 ≤ f.lift g2.

Русский

Если ∀ s ∈ f, g1(s) ≤ g2(s), тогда f.lift g1 ≤ f.lift g2.

LaTeX

$$∀ s ∈ f,\; g1(s) ≤ g2(s) \Rightarrow f.lift g1 ≤ f.lift g2$$

Lean4

theorem lift_mono' (hg : ∀ s ∈ f, g₁ s ≤ g₂ s) : f.lift g₁ ≤ f.lift g₂ :=
  iInf₂_mono hg

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

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

Разделы

Аффилиация

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