lift'_mono'

Mathlib.Order.Filter.Lift

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

English

If hh: ∀ s ∈ f, h1 s ⊆ h2 s, then f.lift' h1 ≤ f.lift' h2.

Русский

Если для каждого s ∈ f выполняется h1 s ⊆ h2 s, то f.lift' h1 ≤ f.lift' h2.

LaTeX

$$$ (hh : \\forall s \\in f, h_1 s \\subseteq h_2 s) \\Rightarrow f.lift' h_1 \\le f.lift' h_2 $$$

Lean4

theorem lift'_mono' (hh : ∀ s ∈ f, h₁ s ⊆ h₂ s) : f.lift' h₁ ≤ f.lift' h₂ :=
  iInf₂_mono fun s hs => principal_mono.mpr <| hh s hs

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

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

Разделы

Аффилиация

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