apply_symm_apply — Mathlib

English

Let h: α ≃ᵤ β be a uniform equivalence. The underlying map h is a bijection between α and β.

Русский

Пусть h: α ≃ᵤ β — равномерное эквивалентство. Заданное им отображение является биекцией между α и β.

LaTeX

$$$\\forall {\\alpha \\beta} [UniformSpace \\alpha] [UniformSpace \\beta] (h : \\alpha \\simeq_u \\beta),\\; h \text{ is bijective}$$$

Lean4

@[simp]
theorem apply_symm_apply (h : α ≃ᵤ β) (x : β) : h (h.symm x) = x :=
  h.toEquiv.apply_symm_apply x

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