homeoFnOfDiscrete_symm_apply — Mathlib

English

The inverse direction of the above equivalence also acts trivially on functions: for any f, the inverse maps back to f.

Русский

Обратное отображение в той же наиболее естественной идентификации отображает f в саму функцию f.

LaTeX

$$$homeoFnOfDiscrete^{-1}(f) = f \quad \forall f: X \to Y$$$

Lean4

@[simp]
theorem homeoFnOfDiscrete_symm_apply (f : X → Y) : homeoFnOfDiscrete.symm f = f :=
  rfl

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