symm_apply_apply — Mathlib

English

Let h: α ≃ᵤ β be a uniform equivalence. For every x in α, h^{-1}(h(x)) = x.

Русский

Пусть h: α ≃ᵤ β — равномерное эквивалентность. Для каждого x ∈ α выполняется h^{-1}(h(x)) = x.

LaTeX

$$$\\forall {\\alpha \\beta} [UniformSpace \\alpha] [UniformSpace \\beta] (h : \\alpha \\simeq_u \\beta),\\; h^{-1}\$h(x)\$ = x$$$

Lean4

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

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