isComplete_iff — Mathlib

English

A map which induces a uniform structure has its domain complete iff its range is complete.

Русский

Отображение, индуцирующее равномерность, имеет полное доменное пространство тогда и только тогда, когда диапазон полон.

LaTeX

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

Lean4

/-- Sets of a subtype are complete iff their image under the coercion is complete. -/
theorem isComplete_iff {p : α → Prop} {s : Set { x // p x }} : IsComplete s ↔ IsComplete ((↑) '' s : Set α) :=
  isUniformEmbedding_subtype_val.isComplete_iff.symm

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