coe_toContinuousMap — Mathlib

English

The natural coercion from a cocompact map to its underlying continuous map is compatible with the function-like coe; i.e., (f.toContinuousMap) equals f as a function.

Русский

Естественная коэрцировка коккомпактной карты к ее базовой непрерывной карте совместима с операцией приведения к функции; то есть (f.toContinuousMap) = f.

LaTeX

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

Lean4

@[simp]
theorem coe_toContinuousMap {f : CocompactMap α β} : (f.toContinuousMap : α → β) = f :=
  rfl

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