OAI/Analysis/BoundedHochschild/WitnessClosure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Countable sets closed under words and prescribed countable witness families.

  1. def OAI.HochschildLocalization.wordSet line 18
  2. lemma OAI.HochschildLocalization.wordSet_countable line 19
  3. lemma OAI.HochschildLocalization.subset_wordSet line 22
  4. lemma OAI.HochschildLocalization.wordSet_mono line 23
  5. theorem OAI.HochschildLocalization.exists_countable_witness_closure line 26