toFilter_mono — Mathlib

English

If l1 ≤ l2, then l1.toFilteriUnion I π0 ≤ l2.toFilteriUnion I π0 for any π0.

Русский

Если l1 ≤ l2, то l1.toFilteriUnion I π0 ≤ l2.toFilteriUnion I π0 для любого π0.

LaTeX

$$$l_1 \\le l_2 \\Rightarrow l_1.toFilteriUnion I \\pi_0 \\le l_2.toFilteriUnion I \\pi_0$$$

Lean4

@[gcongr, mono]
theorem toFilter_mono (I : Box ι) {l₁ l₂ : IntegrationParams} (h : l₁ ≤ l₂) : l₁.toFilter I ≤ l₂.toFilter I :=
  iSup_mono fun _ => toFilterDistortion_mono I h le_rfl

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