English
Let f: X → Y be a continuous map between topological spaces and {U_i} an open cover of Range(f) by opens. Then DenseRange f iff for every i, DenseRange of the restricted map f|_{f^{-1}(U_i)}.
Русский
Пусть f: X → Y непрерывно. Пусть покрытие Range(f) состоит из открытых U_i. Тогда DenseRange(f) эквивалентно DenseRange(ограниченного) f|_{f^{-1}(U_i)} для каждого i.
LaTeX
$$$\operatorname{DenseRange}(f) \iff \forall i,\ \operatorname{DenseRange}\left(f\big|_{f^{-1}(U_i)}\right)$$$
Lean4
theorem denseRange_iff_restrictPreimage : DenseRange f ↔ ∀ i, DenseRange ((U i).1.restrictPreimage f) :=
by
simp_rw [denseRange_iff_closure_range, Set.range_restrictPreimage, ←
(U _).2.isOpenEmbedding_subtypeVal.isOpenMap.preimage_closure_eq_closure_preimage continuous_subtype_val]
simp only [Opens.carrier_eq_coe, SetLike.coe_sort_coe, preimage_eq_univ_iff, Subtype.range_coe_subtype,
SetLike.mem_coe]
rw [← iUnion_subset_iff, ← Set.univ_subset_iff, iff_iff_eq]
congr 1
exact hU.iSup_set_eq_univ.symm
