map_pt — Mathlib

English

For any pointed map f between inhabited types Γ and Γ', the value at the distinguished point (default) is preserved: f(default) = default.

Русский

Для любого отображения с указанной точкой f между непустыми типами Γ и Γ' значение в отмеченной точке сохраняется: f(default) = default.

LaTeX

$$$\forall {\Gamma} {\Gamma'} [Inhabited(\Gamma)] [Inhabited(\Gamma')] (f : PointedMap(\Gamma, \Gamma')):\ f.default = default$$$

Lean4

@[simp]
theorem map_pt {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') : f default = default :=
  PointedMap.map_pt' _

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