continuousMapOfUnique_apply — Mathlib

English

For any y ∈ Y and x ∈ X, the value of the constructed map is y; i.e., the evaluation at x is y.

Русский

Для любых y ∈ Y и x ∈ X значение соответствующего отображения равно y; то есть применение к x возвращает y.

LaTeX

$$$\\text{continuousMapOfUnique}(y)(x) = y$$$

Lean4

@[simp]
theorem continuousMapOfUnique_apply [Unique X] (y : Y) (x : X) : continuousMapOfUnique y x = y :=
  rfl

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