rangeInr — Mathlib

English

`rangeInr` is an equivalence between the range of Sum.inr and β.

Русский

rangeInr — эквивалентность между образами Sum.inr и β.

LaTeX

$$$ \text{rangeInr} : (range Sum.inr) \simeq^ᵐ β $$$

Lean4

/-- `β` is equivalent to its image in `α ⊕ β` as measurable spaces. -/
def rangeInr : (range Sum.inr : Set (α ⊕ β)) ≃ᵐ β
    where
  toEquiv := Equiv.Set.rangeInr α β
  measurable_toFun s
    (hs : MeasurableSet s) := by
    refine ⟨_, hs.inr_image, Set.ext ?_⟩
    simp
  measurable_invFun := Measurable.subtype_mk measurable_inr

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