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)