toEquiv_injective — Mathlib

English

The natural map that sends a uniform equivalence to its underlying equivalence is injective.

Русский

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

LaTeX

$$$\forall a,b:\alpha\simeq\beta,\ (toEquiv(a)=toEquiv(b)\Rightarrow a=b)$$$

Lean4

theorem toEquiv_injective : Function.Injective (toEquiv : α ≃ᵤ β → α ≃ β)
  | ⟨e, h₁, h₂⟩, ⟨e', h₁', h₂'⟩, h => by simpa only [mk.injEq]

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