completeSpace_iff_isComplete_range

English

If f is an inducing map, CompleteSpace α is equivalent to IsComplete (range f).

Русский

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

LaTeX

$$$\\text{completeSpace\\_iff\\_isComplete\\_range}(f)$$$

Lean4

theorem completeSpace_iff_isComplete_range {f : α → β} (hf : IsUniformInducing f) :
    CompleteSpace α ↔ IsComplete (range f) := by
  rw [completeSpace_iff_isComplete_univ, ← isComplete_image_iff hf, image_univ]

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