toFilterDistortion_mono — Mathlib

English

If l1 ≤ l2, then l1.toFilter I ≤ l2.toFilter I for any Box I.

Русский

Если l1 ≤ l2, то для любых Box I выполняется l1.toFilter I ≤ l2.toFilter I.

LaTeX

$$$l_1 \\le l_2 \\Rightarrow l_1.toFilter I \\le l_2.toFilter I$$$

Lean4

@[gcongr, mono]
theorem toFilterDistortion_mono (I : Box ι) (h : l₁ ≤ l₂) (hc : c₁ ≤ c₂) :
    l₁.toFilterDistortion I c₁ ≤ l₂.toFilterDistortion I c₂ :=
  iInf_mono fun _ =>
    iInf_mono' fun hr => ⟨hr.mono h, principal_mono.2 fun _ => MemBaseSet.mono I h hc fun _ _ => le_rfl⟩

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