OAI/Analysis/SeparableQuotients/ProductQuotients.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.hasSQ_of_adjoint_not_SS line 21
2. lemma OAI.SeparableQuotient.norm_dual_prod_le line 38
3. lemma OAI.SeparableQuotient.top_infinite line 58
4. theorem OAI.SeparableQuotient.hasSQ_prod_cases line 66

   Source documentation

   The separable quotient dichotomy for a product, via the evaluation criterion.

   theorem hasSQ_prod_cases (h : HasSeparableQuotient 𝕜 (X × Y)) :
       HasSeparableQuotient 𝕜 X ∨ HasSeparableQuotient 𝕜 Y := by
   …

   Mentions: OAI.SeparableQuotient.HasSeparableQuotient