measurableEmbedding — Mathlib

English

A measurable equivalence is a measurable embedding.

Русский

Измеримая эквивалентность является измеримым вложением.

LaTeX

$$$ \text{MeasurableEmbedding } e $$$

Lean4

/-- A measurable equivalence is a measurable embedding. -/
protected theorem measurableEmbedding (e : α ≃ᵐ β) : MeasurableEmbedding e
    where
  injective := e.injective
  measurable := e.measurable
  measurableSet_image' := fun _ => e.measurableSet_image.2

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