coe_mk — Mathlib

English

The construction that packages a function f with witnesses hf and hf' into a ZeroAtInftyContinuousMap α β yields the original function f.

Русский

Конструкция, превращающая функцию f и доказательства hf, hf' в объект ZeroAtInftyContinuousMap, возвращает саму функцию f.

LaTeX

$${ toFun := f, continuous_toFun := hf, zero_at_infty' := hf' : ZeroAtInftyContinuousMap α β } = f$$

Lean4

@[simp]
theorem coe_mk {f : α → β} (hf : Continuous f) (hf' : Tendsto f (cocompact α) (𝓝 0)) :
    { toFun := f, continuous_toFun := hf, zero_at_infty' := hf' : ZeroAtInftyContinuousMap α β } = f :=
  rfl

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