English
A C*-algebra is spanned by nonnegative elements of norm less than r: span_ℂ({x ∈ A | 0 ≤ x} ∩ Ball(0, r)) = ⊤ for r > 0.
Русский
C*-алгебра порождается неотрицательными элементами с нормой строго меньше r: линейная оболочка их равна всей алгебре.
LaTeX
$$$$\operatorname{span}_{\mathbb{C}}\big\{ x \in A \\ 0 \le x \\ \|x\| < r \big\} = \top, \quad r > 0.$$$$
Lean4
/-- A C⋆-algebra is spanned by nonnegative elements of norm less than `r`. -/
theorem span_nonneg_inter_ball {r : ℝ} (hr : 0 < r) : span ℂ ({x : A | 0 ≤ x} ∩ Metric.ball 0 r) = ⊤ :=
by
rw [eq_top_iff, ← span_nonneg_inter_closedBall (half_pos hr)]
gcongr
exact Metric.closedBall_subset_ball <| half_lt_self hr