map — Mathlib

English

For a continuous map f : α → β and K ∈ Compacts α, the carrier of the image compact equals the image of the carrier: (s.map f hf : Set β) = f '' s.

Русский

Для непрерывного отображения f: α → β и K ∈ Compacts α носитель образа компактного множества равен образу носителя: (s.map f hf : Set β) = f '' s.

LaTeX

$$$\\forall {f : \\alpha \\rightarrow \\beta} (hf : Continuous f) (s : \\mathrm{Compacts}(\\alpha)),\\quad (s.map f hf : \\text{Set }\\beta) = f '' s$$$

Lean4

/-- The image of a compact set under a continuous function. -/
protected def map (f : α → β) (hf : Continuous f) (K : Compacts α) : Compacts β :=
  ⟨f '' K.1, K.2.image hf⟩

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