range_eq_univ — Mathlib

English

An affine isometry equivalence is continuous on every set, hence continuous on all of its domain.

Русский

Аффинная изометрия непрерывна на любом задаваемом множестве, следовательно на всей области определения.

LaTeX

$$$$ \text{ContinuousOn}(e)\quad\text{for } e : P \simeq^{\mathrm{AI}} P_2. $$$$

Lean4

theorem range_eq_univ (e : P ≃ᵃⁱ[𝕜] P₂) : Set.range e = Set.univ :=
  by
  rw [← coe_toIsometryEquiv]
  exact IsometryEquiv.range_eq_univ _

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