preimage — Mathlib

English

Preimage of a dense set under an open map is dense.

Русский

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

LaTeX

$$$Dense(s) \\to IsOpenMap(f) \\to Dense(f^{-1}(s))$$$

Lean4

/-- Preimage of a dense set under an open map is dense. -/
protected theorem preimage {s : Set Y} (hs : Dense s) (hf : IsOpenMap f) : Dense (f ⁻¹' s) := fun x ↦
  hf.preimage_closure_subset_closure_preimage <| hs (f x)

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