range_eq_univ — Mathlib

English

If I is boundaryless, then its range is the whole target space: range I = univ.

Русский

Если I без границы, то образ равен всей целевой области: range I = univ.

LaTeX

$$$\mathrm{range} I = \mathrm{univ}$$$

Lean4

theorem range_eq_univ {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] : range I = univ :=
  ModelWithCorners.Boundaryless.range_eq_univ

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