symm_comp_self — Mathlib

English

If h: α ≃ᵤ β, then h^{-1} ∘ h is the identity on α.

Русский

Если h: α ≃ᵤ β, то обратная карта после самой карты дает тождественное отображение на α.

LaTeX

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

Lean4

@[simp]
theorem symm_comp_self (h : α ≃ᵤ β) : (h.symm : β → α) ∘ h = id :=
  funext h.symm_apply_apply

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