completeSpace_iff — Mathlib

English

CompleteSpace of Separation Quotient α is equivalent to CompleteSpace α.

Русский

Полнота фактор-пространства по сепарационному эквиваленту эквивалентна полноте исходного пространства.

LaTeX

$$$\\text{SeparationQuotient.completeSpace\\_iff}(α)$$$

Lean4

theorem completeSpace_iff : CompleteSpace (SeparationQuotient α) ↔ CompleteSpace α :=
  .symm <| isUniformInducing_mk.completeSpace_congr surjective_mk

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