coe_map — Mathlib

English

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

Русский

Для непрерывного отображения f : α → β и s ∈ 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

@[simp, norm_cast]
theorem coe_map {f : α → β} (hf : Continuous f) (s : Compacts α) : (s.map f hf : Set β) = f '' s :=
  rfl

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