isClosedEmbedding_of_spaced_out — Mathlib

English

If f is spaced-out and has uniform embedding property, then the embedding is closed.

Русский

Если отображение обладает свойством равномерного вложения и разделяется по пространству, то вложение закрытое.

LaTeX

$$$\\text{IsClosedEmbedding}(f)$$$

Lean4

theorem isClosedEmbedding_of_spaced_out {α} [TopologicalSpace α] [DiscreteTopology α] [T0Space β] {f : α → β}
    {s : Set (β × β)} (hs : s ∈ 𝓤 β) (hf : Pairwise fun x y => (f x, f y) ∉ s) : IsClosedEmbedding f :=
  by
  rcases @DiscreteTopology.eq_bot α _ _ with rfl; let _ : UniformSpace α := ⊥
  exact
    { (isUniformEmbedding_of_spaced_out hs hf).isEmbedding with isClosed_range := isClosed_range_of_spaced_out hs hf }

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