completeSpace_congr — Mathlib

English

If f is a surjective uniform inducing map, then CompleteSpace α iff CompleteSpace β.

Русский

Если f — сюръективное равномерно индуцирующее отображение, то пространства полные взаимно эквивалентны.

LaTeX

$$$\\text{completeSpace\\_congr}(f)$$$

Lean4

/-- If `f` is a surjective uniform inducing map,
then its domain is a complete space iff its codomain is a complete space.
See also `_root_.completeSpace_congr` for a version that assumes `f` to be an equivalence. -/
theorem completeSpace_congr {f : α → β} (hf : IsUniformInducing f) (hsurj : f.Surjective) :
    CompleteSpace α ↔ CompleteSpace β := by
  rw [completeSpace_iff_isComplete_range hf, hsurj.range_eq, completeSpace_iff_isComplete_univ]

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