isUniformEmbedding_of_spaced_out — Mathlib

English

If s is spaced-out and f(x) for x in α preserves non-membership of s for distinct points, then f is a uniform embedding.

Русский

Если f сохраняет разреженность по отношению к s для различных x, y, то f — равномерное вложение.

LaTeX

$$$\\text{IsUniformEmbedding}(f)$ under spaced-out condition$$

Lean4

/-- If a map `f : α → β` sends any two distinct points to point that are **not** related by a fixed
`s ∈ 𝓤 β`, then `f` is a uniform embedding with respect to the discrete uniformity on `α`. -/
theorem isUniformEmbedding_of_spaced_out {α} {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β)
    (hf : Pairwise fun x y => (f x, f y) ∉ s) : @IsUniformEmbedding α β ⊥ ‹_› f :=
  by
  let _ : UniformSpace α := ⊥; have := discreteTopology_bot α
  exact IsUniformInducing.isUniformEmbedding ⟨comap_uniformity_of_spaced_out hs hf⟩

Похожие утверждения