toFilteriUnion_mono — Mathlib

English

If π1.iUnion = π2.iUnion, then l.toFilteriUnion I π1 = l.toFilteriUnion I π2.

Русский

Если π1.iUnion = π2.iUnion, то l.toFilteriUnion I π1 = l.toFilteriUnion I π2.

LaTeX

$$$\\pi_1.iUnion = \\pi_2.iUnion \\Rightarrow l.toFilteriUnion I \\pi_1 = l.toFilteriUnion I \\pi_2$$$

Lean4

@[gcongr, mono]
theorem toFilteriUnion_mono (I : Box ι) {l₁ l₂ : IntegrationParams} (h : l₁ ≤ l₂) (π₀ : Prepartition I) :
    l₁.toFilteriUnion I π₀ ≤ l₂.toFilteriUnion I π₀ :=
  iSup_mono fun _ => inf_le_inf_right _ <| toFilterDistortion_mono _ h le_rfl

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