image — Mathlib

English

The image of a separable set under a continuous map is separable.

Русский

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

LaTeX

$$$IsSeparable(s) \rightarrow (\forall f, Continuous f) \rightarrow IsSeparable(f''s)$$$

Lean4

theorem image {β : Type*} [TopologicalSpace β] {s : Set α} (hs : IsSeparable s) {f : α → β} (hf : Continuous f) :
    IsSeparable (f '' s) := by
  rcases hs with ⟨c, c_count, hc⟩
  refine ⟨f '' c, c_count.image _, ?_⟩
  rw [image_subset_iff]
  exact hc.trans (closure_subset_preimage_closure_image hf)

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