English
Suppose i : α → β is accompanied by a continuous i, a dense range condition, injectivity, and a neighborhood lifting property H. Then i is a dense inducing map.
Русский
Пусть i : α → β сопутствует непрерывный переход, плотность образа и инъективность, а также условие H о подъёме окрестностей. Тогда i является плотным индуцирующим отображением.
LaTeX
$$$(\\\\forall a: \\alpha)\\\\;\\\\dots \\\\Rightarrow \\\\ IsDenseInducing(i)$$$
Lean4
theorem mk' (i : α → β) (c : Continuous i) (dense : ∀ x, x ∈ closure (range i))
(H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (i a), ∀ b, i b ∈ t → b ∈ s) : IsDenseInducing i
where
toIsInducing := isInducing_iff_nhds.2 fun a => le_antisymm (c.tendsto _).le_comap (by simpa [Filter.le_def] using H a)
dense := dense
