toEquiv_inj — Mathlib

English

A stronger form: equality of the underlying equivalences is equivalent to equality of the semilinear equivalences themselves.

Русский

Справедливо и более сильное утверждение: равенство базовых эквивалентностей эквивалентно равенству самих семилинейных эквивалентностей.

LaTeX

$$$e_1.toEquiv = e_2.toEquiv \iff e_1 = e_2$$$

Lean4

@[simp]
theorem toEquiv_inj {e₁ e₂ : M ≃ₛₗ[σ] M₂} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂ :=
  toEquiv_injective.eq_iff

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