OAI/Analysis/BoundedHochschild/WeakSubspaces.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Preannihilators, quotient duals and weak-star closed subspaces.

  1. def OAI.BoundedHochschild.WeakSubspace.preannihilator line 28
  2. lemma OAI.BoundedHochschild.WeakSubspace.preannihilator_closed line 34
  3. lemma OAI.BoundedHochschild.WeakSubspace.mem_iff_annihilates line 43
  4. def OAI.BoundedHochschild.WeakSubspace.strong line 80
  5. lemma OAI.BoundedHochschild.WeakSubspace.mem_strong line 83
  6. instance OAI.BoundedHochschild.WeakSubspace.preannihilator_closed_instance line 93
  7. lemma OAI.BoundedHochschild.WeakSubspace.quotient_dual_norm line 96
  8. def OAI.BoundedHochschild.WeakSubspace.quotientDual line 123
  9. lemma OAI.BoundedHochschild.WeakSubspace.quotientDual_surjective line 135
  10. def OAI.BoundedHochschild.WeakSubspace.quotientDualEquiv line 149
  11. lemma OAI.BoundedHochschild.traceVector_star_pairing line 176
  12. theorem OAI.BoundedHochschild.exists_star_preadjoint line 185
  13. lemma OAI.BoundedHochschild.predual_tendsto_star line 217