piLE_eq_comap_frestrictLe — Mathlib

English

For locally finite order ι, the i-th level of piLE equals the comap of frestrictLe i on π, i.e., piLE.seq i = pi.comap (frestrictLe i).

Русский

Для локально конечного порядка ι i‑й уровень piLE равен сопряжению frestrictLe i на π: piLE.seq i = pi.comap (frestrictLe i).

LaTeX

$$$\\text{piLE.seq } i = \\text{pi.comap}(\\text{frestrictLe } i)$$$

Lean4

theorem piLE_eq_comap_frestrictLe (i : ι) : piLE (X := X) i = pi.comap (frestrictLe i) :=
  by
  apply le_antisymm
  · simp_rw [piLE, ← piCongrLeft_comp_frestrictLe, ← MeasurableEquiv.coe_piCongrLeft, ← comap_comp]
    exact MeasurableSpace.comap_mono <| Measurable.comap_le (by fun_prop)
  · rw [← piCongrLeft_comp_restrictLe, ← MeasurableEquiv.coe_piCongrLeft, ← comap_comp]
    exact MeasurableSpace.comap_mono <| Measurable.comap_le (by fun_prop)

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