generateMeasurableRec_mono — Mathlib

English

The map i ↦ generateMeasurableRec s i is monotone with respect to i.

Русский

Отображение i ↦ generateMeasurableRec s i монотонно по отношению к i.

LaTeX

$$$\\operatorname{Monotone}(\\mathrm{generateMeasurableRec}(s))$$$

Lean4

theorem generateMeasurableRec_mono (s : Set (Set α)) : Monotone (generateMeasurableRec s) :=
  by
  intro i j h x hx
  rcases h.eq_or_lt with (rfl | h)
  · exact hx
  · convert iUnion_mem_generateMeasurableRec fun _ => ⟨i, h, hx⟩
    exact (iUnion_const x).symm

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