hasBasis_approximateUnit — Mathlib

English

The canonical approximate unit has a basis given by the sets S_a = { x ∈ A : a ≤ x } ∩ closedBall(0,1) for all a ≥ 0.

Русский

Каноническая приближенная единица имеет базис, задаваемый множествами S_a = { x ∈ A : a ≤ x } ∩ замкнутый шар 0-1 при всех a ≥ 0.

LaTeX

$$$(\operatorname{approximateUnit}(A)).\text{HasBasis} (\text{fun } x:\, A \to 0 \le x \land \|x\| < 1)\left(\{x \mid \cdot \le x\} \cap \overline{B}(0,1)\right)$$$

Lean4

/-- The canonical approximate unit in a C⋆-algebra has a basis of sets
`{x | a ≤ x} ∩ closedBall 0 1` for `0 ≤ a`. -/
theorem hasBasis_approximateUnit :
    (approximateUnit A).HasBasis (fun x : A ↦ 0 ≤ x ∧ ‖x‖ < 1) ({x | · ≤ x} ∩ closedBall 0 1) :=
  isBasis_nonneg_sections A |>.hasBasis.inf_principal (closedBall 0 1)

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