English
In a nonunital C*-algebra A with a compatible order structure, the set of nonnegative elements {a ∈ A | 0 ≤ a} is closed in the topology of A.
Русский
В неполной C*-алгебре A с совместимой порядковой структурой множество неотрицательных элементов {a ∈ A | 0 ≤ a} замкнуто в топологии A.
LaTeX
$$$\\{a \\in A \\mid 0 \\le a\\} \\text{ is closed in } A.$$$
Lean4
/-- The set of nonnegative elements in a C⋆-algebra is closed. -/
theorem isClosed_nonneg : IsClosed {a : A | 0 ≤ a} :=
by
suffices IsClosed {a : A⁺¹ | 0 ≤ a}
by
rw [Unitization.isometry_inr (𝕜 := ℂ) |>.isClosedEmbedding.isClosed_iff_image_isClosed]
convert this.inter <| (Unitization.isometry_inr (𝕜 := ℂ)).isClosedEmbedding.isClosed_range
ext a
simp only [Set.mem_image, Set.mem_setOf_eq, Set.mem_inter_iff, Set.mem_range, ← exists_and_left]
congr! 2 with x
exact and_congr_left fun h ↦ by simp [← h]
simp only [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts,
and_congr_right (SpectrumRestricts.nnreal_iff_nnnorm · le_rfl), Set.setOf_and]
refine isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_
all_goals fun_prop
