mkOfCompact_apply

Mathlib.Topology.ContinuousMap.Bounded.Basic

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

English

Evaluation is preserved: for [CompactSpace α], (mkOfCompact f) a = f a.

Русский

Оценка сохраняется: для компактного пространства α выполняется (mkOfCompact f) a = f a.

LaTeX

$$$[\text{CompactSpace } \alpha] (f : C(\alpha, \beta)) \; (a : \alpha) :\; mkOfCompact f a = f a$$$

Lean4

@[simp]
theorem mkOfCompact_apply [CompactSpace α] (f : C(α, β)) (a : α) : mkOfCompact f a = f a :=
  rfl

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

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

Разделы

Аффилиация

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