expMap_source — Mathlib

English

The source of expMap is the universal set in realSpace K.

Русский

Область определения expMap есть все пространство realSpace K.

LaTeX

$$$\\mathrm{expMap}.\\mathrm{source} = (\\mathrm{Set.univ} : \\mathrm{Set} (\\mathrm{realSpace} K))$$$

Lean4

theorem expMap_source : expMap.source = (Set.univ : Set (realSpace K)) := by
  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_source, expMap_single, Set.pi_univ Set.univ]

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