map — Mathlib

English

The image of a compact-open set under a continuous open map is again compact-open.

Русский

Образ компактно-открытого множества под действием непрерывного открытого отображения снова компактно-открыто.

LaTeX

$$map (f) hf hf' : CompactOpens α → CompactOpens β$$

Lean4

/-- The image of a compact open under a continuous open map. -/
@[simps toCompacts]
def map (f : α → β) (hf : Continuous f) (hf' : IsOpenMap f) (s : CompactOpens α) : CompactOpens β :=
  ⟨s.toCompacts.map f hf, hf' _ s.isOpen⟩

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