compactlySupported_eq_top_of_isCompact

English

If α is compact, then every bounded continuous function α → γ has compact support, hence C_cb(α, γ) = ⊤.

Русский

Если пространство α компактно, то любая ограниченно непрерывная функция α→γ имеет компактную опору, следовательно C_cb(α, γ) = ⊤.

LaTeX

$$$IsCompact(Set.univ) \\Rightarrow C_{cb}(\\alpha, \\gamma) = \\top$$$

Lean4

theorem compactlySupported_eq_top_of_isCompact (h : IsCompact (Set.univ : Set α)) : C_cb(α, γ) = ⊤ :=
  eq_top_iff.mpr fun _ _ ↦
    h.of_isClosed_subset (isClosed_tsupport _)
      (subset_univ _)
        /- This is intentionally not marked `@[simp]` to prevent Lean looking for a `CompactSpace α`
        instance every time it sees `C_cb(α, γ)`. -/

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