measurable_comp_iff — Mathlib

English

For any f: β → γ and a measurable equivalence e: α ≃ᵐ β, Measurable (f ∘ e) iff Measurable f.

Русский

Для любого f: β → γ и измеримой эквивалентности e: α ≃ᵐ β верно: Measurable(f ∘ e) ⇔ Measurable f.

LaTeX

$$$ \text{Measurable } (f \circ e) \iff \text{Measurable } f $$$

Lean4

protected theorem measurable_comp_iff {f : β → γ} (e : α ≃ᵐ β) : Measurable (f ∘ e) ↔ Measurable f :=
  Iff.intro
    (fun hfe => by
      have : Measurable (f ∘ (e.symm.trans e).toEquiv) := hfe.comp e.symm.measurable
      rwa [coe_toEquiv, symm_trans_self] at this)
    fun h => h.comp e.measurable

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