monotone_iUnionUpTo — Mathlib

English

The map iUnionUpTo from the Besicovitch TauPackage is monotone: if i ≤ j then p.iUnionUpTo i ⊆ p.iUnionUpTo j.

Русский

Показатель iUnionUpTo в пакете Besicovitch TauPackage монотонен: если i ≤ j, то p.iUnionUpTo i ⊆ p.iUnionUpTo j.

LaTeX

$$$\text{Monotone}(p.iUnionUpTo)$, i.e. for all i,j,\; i \le j \Rightarrow p.iUnionUpTo(i) \subseteq p.iUnionUpTo(j).$$$

Lean4

theorem monotone_iUnionUpTo : Monotone p.iUnionUpTo :=
  by
  intro i j hij
  simp only [iUnionUpTo]
  exact iUnion_mono' fun r => ⟨⟨r, r.2.trans_le hij⟩, Subset.rfl⟩

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