coe_ofNormedAddCommGroupDiscrete — Mathlib

English

Similarly to the previous result, the coercion of a discretely-defined bounded continuous function equals the original function.

Русский

Аналогично предыдущему результату, тождество отображения ограниченной непрерывной функции сохраняется при дискретизации.

LaTeX

$$$(\text{coe_ofNormedAddCommGroupDiscrete } f\, C\, H) = f$$$

Lean4

@[simp]
theorem coe_ofNormedAddCommGroupDiscrete {α : Type u} {β : Type v} [TopologicalSpace α] [DiscreteTopology α]
    [SeminormedAddCommGroup β] (f : α → β) (C : ℝ) (H : ∀ x, ‖f x‖ ≤ C) :
    (ofNormedAddCommGroupDiscrete f C H : α → β) = f :=
  rfl

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