toHomeomorph_inj — Mathlib

English

For f,g: E ≃ₛₗᵢ[σ₁₂] E₂, f.toHomeomorph = g.toHomeomorph if and only if f = g.

Русский

Для любых f,g: E ≃ₛₗᵢ[σ₁₂] E₂ верно: f.toHomeomorph = g.toHomeomorph тогда и только тогда, когда f = g.

LaTeX

$$$f.toHomeomorph = g.toHomeomorph \\iff f = g$$$

Lean4

@[simp]
theorem toHomeomorph_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toHomeomorph = g.toHomeomorph ↔ f = g :=
  toHomeomorph_injective.eq_iff

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