OAI/Analysis/Nuclearity/PositiveConeSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weak-star separation step used in KR02 Lemma 7.17(ii). A separating continuous functional on the weak dual is evaluation at an actual self-adjoint algebra element.

  1. lemma OAI.WeakPureInfiniteness.selfAdjoint_separator_of_closed_cone line 16