isComplete_range — Mathlib

English

If f is IsUniformInducing and α is complete, then range f is complete.

Русский

Если f является равномерно-индуцирующим и пространство α полно, то диапазон f полно.

LaTeX

$$[CompleteSpace α] (hf : IsUniformInducing f) → IsComplete (range f)$$

Lean4

theorem isComplete_range [CompleteSpace α] (hf : IsUniformInducing f) : IsComplete (range f) :=
  (completeSpace_iff_isComplete_range hf).1 ‹_›

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