equivOfIsEmbeddingOfRangeEq_apply_infty

Mathlib.Topology.Compactification.OnePoint.Basic

URI: https://scilib.ai/kg/mathlib#OnePoint.equivOfIsEmbeddingOfRangeEq_apply_infty

English

For x in X, the forward direction of the equivalence evaluates to f(x).

Русский

Для x из X отображение в эквиваленте даёт f(x).

LaTeX

$$$\\mathrm{equivOfIsEmbeddingOfRangeEq}\\; y\\; f\\; hf\\; hy\\; x = f(x).$$$

Lean4

@[simp]
theorem equivOfIsEmbeddingOfRangeEq_apply_infty : equivOfIsEmbeddingOfRangeEq y f hf hy ∞ = y :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru