English
If s is spaced-out and f respects that, then f is a uniform embedding.
Русский
Если s разбросано по β×β и f сохраняет это, то f — равномерное вложение.
LaTeX
$$$\\text{IsUniformEmbedding}(f)$ under spaced-out condition$$
Lean4
theorem closure_image_mem_nhds_of_isUniformInducing {s : Set (α × α)} {e : α → β} (b : β) (he₁ : IsUniformInducing e)
(he₂ : IsDenseInducing e) (hs : s ∈ 𝓤 α) : ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b :=
by
obtain ⟨U, ⟨hU, hUo, hsymm⟩, hs⟩ : ∃ U, (U ∈ 𝓤 β ∧ IsOpen U ∧ IsSymmetricRel U) ∧ Prod.map e e ⁻¹' U ⊆ s := by
rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs
rcases he₂.dense.mem_nhds (UniformSpace.ball_mem_nhds b hU) with ⟨a, ha⟩
refine ⟨a, mem_of_superset ?_ (closure_mono <| image_mono <| UniformSpace.ball_mono hs a)⟩
have ho : IsOpen (UniformSpace.ball (e a) U) := UniformSpace.isOpen_ball (e a) hUo
refine mem_of_superset (ho.mem_nhds <| (UniformSpace.mem_ball_symmetry hsymm).2 ha) fun y hy => ?_
refine mem_closure_iff_nhds.2 fun V hV => ?_
rcases he₂.dense.mem_nhds (inter_mem hV (ho.mem_nhds hy)) with ⟨x, hxV, hxU⟩
exact ⟨e x, hxV, mem_image_of_mem e hxU⟩
