English
The canonical approximate unit forms an increasing approximate unit: the filter of approximate unit is increasing in the natural order of A; left and right tendsto properties hold with respect to this filter, and the filter is nontrivial.
Русский
Каноническая приближенная единица образует возрастающую приближённую единицу: фильтр приближенной единицы возрастает в естественном порядке на A; выполняются свойства стремления слева и справа к этому фильтру, фильтр не тривиален.
LaTeX
$$$\text{increasingApproximateUnit}(A) :\; \operatorname{IsIncreasingApproximateUnit}(\operatorname{approximateUnit}(A))$$$
Lean4
/-- The filter `CStarAlgebra.approximateUnit` generated by the sections
`{x | a ≤ x} ∩ closedBall 0 1` for `0 ≤ a` forms an increasing approximate unit. -/
theorem increasingApproximateUnit : IsIncreasingApproximateUnit (approximateUnit A)
where
tendsto_mul_left := by
rw [tendsto_mul_left_iff_tendsto_mul_right]
· exact tendsto_mul_right_approximateUnit
· rw [(hasBasis_approximateUnit A).eventually_iff]
peel (hasBasis_approximateUnit A).ex_mem with x hx
exact ⟨hx, fun y hy ↦ (hx.1.trans hy.1).isSelfAdjoint⟩
tendsto_mul_right := tendsto_mul_right_approximateUnit
eventually_nonneg := .filter_mono inf_le_left <| (isBasis_nonneg_sections A).hasBasis.eventually_iff.mpr ⟨0, by simp⟩
eventually_norm := .filter_mono inf_le_right <| by simp
neBot := hasBasis_approximateUnit A |>.neBot_iff.mpr fun hx ↦ ⟨_, ⟨le_rfl, by simpa using hx.2.le⟩⟩
