English
A variant of norm_sub_mul_self_le that passes to the unitization: if x ≤ y with x ≥ 0 and ||y|| ≤ 1, then for z in A, and c ∈ ℝ, if ||star(z : A⁺¹) · (1 − x) · z|| ≤ c², then ||z − y · z|| ≤ c.
Русский
Вариант norm_sub_mul_self_le, который переходит к единице: если x ≤ y, x ≥ 0, ||y|| ≤ 1, тогда для z ∈ A и c ∈ ℝ, если ||star(z) · (1 − x) · z|| ≤ c², то ||z − y z|| ≤ c.
LaTeX
$$$\forall z:\, A,\; hx_0: 0 \le x, \ hxy: x \le y, \ hy_1: \|y\| \le 1, \; c: \mathbb{R}, \; (h: \|\star (z) (1 - x) z\| \le c^{2}) \Rightarrow \|z - y z\| \le c$$$
Lean4
@[simp]
theorem norm_star (x : E) : ‖x⋆‖ = ‖x‖ :=
le_antisymm (NormedStarGroup.norm_star_le x) (by simpa using NormedStarGroup.norm_star_le x⋆)
