toEquiv_injective — Mathlib

English

The map that sends a measurable equivalence to its underlying Equiv is injective; distinct measurable equivalences have different underlying Equivs.

Русский

Отображение, отправляющее измеримое эквивалентное отображение в соответствующее обычное эквивалентное отображение, инъективно.

LaTeX

$$$$ \text{Injective}(\text{toEquiv} : \alpha \simeq_{m} \beta \to \alpha \simeq \beta). $$$$

Lean4

theorem toEquiv_injective : Injective (toEquiv : α ≃ᵐ β → α ≃ β) :=
  by
  rintro ⟨e₁, _, _⟩ ⟨e₂, _, _⟩ (rfl : e₁ = e₂)
  rfl

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