expMap_target — Mathlib

English

The target of expMap is the product space of positive reals over all places.

Русский

Цель expMap — это произведение областей положительных вещественных чисел по всем местам.

LaTeX

$$$\\operatorname{expMap}.\\mathrm{target} = (\\mathrm{Set.univ} )^{\\pi} \\;\\mathrm{Ioi} 0$$$

Lean4

theorem expMap_target : expMap.target = Set.univ.pi fun (_ : InfinitePlace K) ↦ Set.Ioi 0 := by
  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_target, expMap_single]

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