isClosedEmbedding — Mathlib

English

If f: α → β is a uniform embedding with α complete and β T0, then f is a closed embedding.

Русский

Пусть f: α → β является равномерным вложением, α полно, β удовлетворяет T0; тогда f является замкнутым вложением.

LaTeX

$$$\\forall f\\colon \\alpha \\to \\beta,\\ IsUniformEmbedding f \\\\Rightarrow \\\\ IsClosedEmbedding f$ with $[UniformSpace\\alpha],[UniformSpace\\beta],[CompleteSpace\\alpha],[T0Space\\beta]$$$

Lean4

theorem isClosedEmbedding [UniformSpace α] [UniformSpace β] [CompleteSpace α] [T0Space β] {f : α → β}
    (hf : IsUniformEmbedding f) : IsClosedEmbedding f :=
  ⟨hf.isEmbedding, hf.isUniformInducing.isComplete_range.isClosed⟩

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