range_eq_univ — Mathlib

English

For any linear isometry equivalence e: E ≃ₛₗᵢ[σ₁₂] E₂, its range is all of E₂; i.e., e is surjective.

Русский

Для любой линейно изометрической эквивалентности e: E ≃ₛₗᵢ[σ₁₂] E₂ ее образ равен всему E₂; то есть e сюръективна.

LaTeX

$$$\mathrm{Set.range}(e) = \mathrm{Set.univ}$$$

Lean4

theorem range_eq_univ (e : E ≃ₛₗᵢ[σ₁₂] E₂) : Set.range e = Set.univ :=
  by
  rw [← coe_toIsometryEquiv]
  exact IsometryEquiv.range_eq_univ _

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