equiv_symm — Mathlib

English

The equivalence induced by the inverse homeomorphism equals the inverse of the forward equivalence: Compacts.equiv f.symm = (Compacts.equiv f).symm.

Русский

Эквивалентность, порождаемая обратным гомеоморфизмом, равна обратной эквиваленции от исходной: Compacts.equiv f.symm = (Compacts.equiv f).symm.

LaTeX

$$$\\mathrm{Compacts.equiv} (f.symm) = (\\mathrm{Compacts.equiv} f)^{-1}$$$

Lean4

@[simp]
theorem equiv_symm (f : α ≃ₜ β) : Compacts.equiv f.symm = (Compacts.equiv f).symm :=
  rfl

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