mkOfCompact — Mathlib

English

A continuous map on a compact space is automatically a bounded continuous function.

Русский

Непрерывное отображение на компактном пространстве автоматически является ограниченно непрерывной функцией.

LaTeX

$$$mkOfCompact [CompactSpace \alpha] (f : C(\alpha, \beta)) : \alpha \to^b \beta$$$

Lean4

/-- A continuous function on a compact space is automatically a bounded continuous function. -/
def mkOfCompact [CompactSpace α] (f : C(α, β)) : α →ᵇ β :=
  ⟨f, isBounded_range_iff.1 (isCompact_range f.continuous).isBounded⟩

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