lift'_mono

Mathlib.Order.Filter.Lift

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

English

If f1 ≤ f2 and h1 ≤ h2 then f1.lift' h1 ≤ f2.lift' h2.

Русский

Если f1 ≤ f2 и h1 ≤ h2, то f1.lift' h1 ≤ f2.lift' h2.

LaTeX

$$$ (hf : f_1 \\le f_2) (hh : h_1 \\le h_2) \\Rightarrow f_1.lift' h_1 \\le f_2.lift' h_2 $$$

Lean4

theorem lift'_mono (hf : f₁ ≤ f₂) (hh : h₁ ≤ h₂) : f₁.lift' h₁ ≤ f₂.lift' h₂ :=
  lift_mono hf fun s => principal_mono.mpr <| hh s

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

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

Разделы

Аффилиация

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