isComplete_iff — Mathlib

English

Sets in a subtype are complete iff their image under the coercion is complete.

Русский

Множества подтипа полные тогда и только тогда, когда их образ при коэффициенте проекции полный.

LaTeX

$$$\\text{IsComplete}(s) \\iff \\text{IsComplete}((\\uparrow)''s)$$$

Lean4

/-- If `f : X → Y` is an `IsUniformEmbedding`, the image `f '' s` of a set `s` is complete
  if and only if `s` is complete. -/
theorem isComplete_iff {f : α → β} {s : Set α} (hf : IsUniformEmbedding f) : IsComplete (f '' s) ↔ IsComplete s :=
  hf.isUniformInducing.isComplete_iff

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