English
Let x be an element of the mixed space over K and w a real place. Then the first component of the element (negAt (signSet x) x) at w equals the absolute value of the first component of x at w; i.e., (negAt (signSet x) x).1 w = |x.1 w| for every real place w.
Русский
Пусть x — элемент смешанного пространства над полем K, и w — вещественное место. Тогда первая компонента после применения negAt к signSet x к x в точке w равна модулю x.1 w: (negAt (signSet x) x).1 w = |x.1 w| для каждого вещественного места w.
LaTeX
$$$\forall x\in \text{mixedSpace}(K),\forall w\in \{ w: \text{InfinitePlace}(K) \mid \ text{IsReal}(w) \},\ (negAt (signSet x) x)_1(w)=|x_1(w)|$$$
Lean4
@[simp]
theorem negAt_signSet_apply_isReal (x : mixedSpace K) (w : { w // IsReal w }) : (negAt (signSet x) x).1 w = ‖x.1 w‖ :=
by
by_cases hw : x.1 w ≤ 0
· rw [negAt_apply_isReal_and_mem _ hw, Real.norm_of_nonpos hw]
· rw [negAt_apply_isReal_and_notMem _ hw, Real.norm_of_nonneg (lt_of_not_ge hw).le]
