map — Mathlib

English

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

Русский

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

LaTeX

$$$ \text{PositiveCompacts.map } f\; hf\; hf'\; s : \mathrm{PositiveCompacts}\, \beta, $$$

Lean4

/-- The image of a positive compact set under a continuous open map. -/
protected def map (f : α → β) (hf : Continuous f) (hf' : IsOpenMap f) (K : PositiveCompacts α) : PositiveCompacts β :=
  { Compacts.map f hf K.toCompacts with
    interior_nonempty' := (K.interior_nonempty'.image _).mono (hf'.image_interior_subset K.toCompacts) }

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