span_nonneg_inter_ball — Mathlib

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

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