OAI/Analysis/Nuclearity/ProductPureSeparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The implication from product-pure-state ideal separation to elementary ideal generation (Tomiyama, Tohoku Math. J. 19 (1967), Theorem 5, combined with pure-state excision). The separation property is an explicit hypothesis of this implication.

  1. structure OAI.WeakPureInfiniteness.ProductPureFunctional line 19
  2. def OAI.WeakPureInfiniteness.ProductPureStateSeparation line 33

    Source documentation

    The product-pure-state separation condition in Tomiyama's Theorem 5.

    def ProductPureStateSeparation : Prop :=
…
  3. theorem OAI.WeakPureInfiniteness.elementary_ideal_generation_of_product_pure_separation line 40
  4. theorem OAI.WeakPureInfiniteness.elementary_span_of_product_pure_separation line 63