mkOfBound_coe

Mathlib.Topology.ContinuousMap.Bounded.Basic

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.mkOfBound_coe

English

The underlying function of mkOfBound is f.

Русский

Базовая функция mkOfBound равна f.

LaTeX

$$$(mkOfBound f C h : \alpha \to \beta) = (f : \alpha \to \beta)$$$

Lean4

@[simp]
theorem mkOfBound_coe {f} {C} {h} : (mkOfBound f C h : α → β) = (f : α → β) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru