isComplete_image_iff — Mathlib

English

If f is a semilinear isometry, then a subset S of E is complete iff its image f''S is complete in E₂.

Русский

Пусть f — полулинейная изометрия. Тогда множество S ⊆ E полно iff его образ f''S полно в E₂.

LaTeX

$$IsComplete(f''S) \Leftrightarrow IsComplete(S)$$

Lean4

theorem isComplete_image_iff [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) {s : Set E} :
    IsComplete (f '' s) ↔ IsComplete s :=
  _root_.isComplete_image_iff (SemilinearIsometryClass.isometry f).isUniformInducing

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