English
Given i, a continuous i, a dense condition, injectivity and a neighborhood lifting condition H, one obtains IsDenseInducing i.
Русский
При данных i, непрерывном i, плотной области, инъективности и условии H по подъёму окрестностей, имеем IsDenseInducing i.
LaTeX
$$$(i : \\alpha \\to \\beta) (c : Continuous\\ i) (dense : \\forall x, x \\in \\overline{\\mathrm{range}\\ i}) (H : \\forall (a : \\alpha), \\forall s \\in 𝓝 a, \\exists t \\in 𝓝 (i a), \\forall b, i b \\in t \\to b \\in s) \\\\Rightarrow IsDenseInducing i$$$
Lean4
theorem isDenseInducing (de : IsDenseEmbedding e) : IsDenseInducing e :=
de.toIsDenseInducing