coe_toContinuousMap — Mathlib

English

Let f be a vanishing-at-infinity continuous map from α to β. The function underlying its associated continuous map is equal to f.

Русский

Пусть f—непрерывное отображение, vanishing at infinity, из α в β. Функция, лежащая в основе связанного с ним отображения, равна f.

LaTeX

$$$ (f.toContinuousMap : \alpha \to \beta) = f $$$

Lean4

@[simp]
theorem coe_toContinuousMap (f : C₀(α, β)) : (f.toContinuousMap : α → β) = f :=
  rfl

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