English
A variant of the previous statement for passing to the unitization: for x ≤ y with x ≥ 0 and ||y|| ≤ 1, if ||star(z in unitization) · (1 − x) · z|| ≤ c², then ||z − y z|| ≤ c.
Русский
Вариант для перехода к аппроксимационной единице: для x ≤ y с x ≥ 0 и ||y|| ≤ 1, если ||star(z) (1 − x) z|| ≤ c² в метризации единицы, то ||z − y z|| ≤ c.
LaTeX
$$$\forall x,y : A, \ hx_0 : 0 \le x, \ hxy : x \le y, \ hy_1 : \|y\| \le 1, \; c \ge 0, \; \big\|\star (z : A^{+1}) (1 - x) z\big\| \le c^{2} \Rightarrow \| z - y z \| \le c$$$
Lean4
/-- A variant of `norm_sub_mul_self_le` for non-unital algebras that passes to the unitization. -/
theorem norm_sub_mul_self_le_of_inr {x y : A} (z : A) (hx₀ : 0 ≤ x) (hxy : x ≤ y) (hy₁ : ‖y‖ ≤ 1) {c : ℝ} (hc : 0 ≤ c)
(h : ‖star (z : A⁺¹) * (1 - x) * z‖ ≤ c ^ 2) : ‖z - y * z‖ ≤ c :=
by
rw [← norm_inr (𝕜 := ℂ), inr_sub, inr_mul]
refine norm_sub_mul_self_le _ ?_ ?_ hc h
· rwa [inr_nonneg_iff]
· have hy := hx₀.trans hxy
rw [Set.mem_Icc, inr_le_iff _ _ hx₀.isSelfAdjoint hy.isSelfAdjoint, ← norm_le_one_iff_of_nonneg _, norm_inr]
exact ⟨hxy, hy₁⟩
