OAI/Computability/WitnessedChoice/Hereditary.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WitnessedSeparation.Hereditary.mk_out line 15
  2. theorem OAI.WitnessedSeparation.Hereditary.isSet_mk line 17
  3. theorem OAI.WitnessedSeparation.Hereditary.isSet_atom line 19
  4. theorem OAI.WitnessedSeparation.Hereditary.elements_mk line 21
  5. theorem OAI.WitnessedSeparation.Hereditary.elements_atom line 23
  6. theorem OAI.WitnessedSeparation.Hereditary.not_mem_atom line 28
  7. theorem OAI.WitnessedSeparation.Hereditary.atom_injective line 32
  8. theorem OAI.WitnessedSeparation.Hereditary.isSet_ofFinset line 38
  9. theorem OAI.WitnessedSeparation.Hereditary.elements_ofFinset line 40
  10. theorem OAI.WitnessedSeparation.Hereditary.mem_ofFinset line 53
  11. theorem OAI.WitnessedSeparation.Hereditary.ext_sets line 57
  12. theorem OAI.WitnessedSeparation.Hereditary.ofFinset_elements line 78
  13. theorem OAI.WitnessedSeparation.Hereditary.atom_or_set line 84
  14. theorem OAI.WitnessedSeparation.Hereditary.rank_mk line 92
  15. theorem OAI.WitnessedSeparation.Hereditary.rank_atom line 94
  16. theorem OAI.WitnessedSeparation.Hereditary.mem_wellFounded line 96
  17. theorem OAI.WitnessedSeparation.Hereditary.map_atom line 99
  18. theorem OAI.WitnessedSeparation.Hereditary.isSet_map line 101
  19. theorem OAI.WitnessedSeparation.Hereditary.elements_map line 105
  20. theorem OAI.WitnessedSeparation.Hereditary.map_ofFinset line 123
  21. def OAI.WitnessedSeparation.Hereditary.mapEquiv line 131
  22. theorem OAI.WitnessedSeparation.Hereditary.smul_atom line 143
  23. theorem OAI.WitnessedSeparation.Hereditary.smul_ofFinset line 146
  24. def OAI.WitnessedSeparation.Hereditary.Supports line 149
  25. def OAI.WitnessedSeparation.Hereditary.Supported line 153
  26. def OAI.WitnessedSeparation.Hereditary.HereditarilySupported line 156
  27. theorem OAI.WitnessedSeparation.Hereditary.ofFinset_inj line 169
  28. theorem OAI.WitnessedSeparation.Hereditary.mem_singleton line 172
  29. theorem OAI.WitnessedSeparation.Hereditary.mem_double line 174
  30. theorem OAI.WitnessedSeparation.Hereditary.singleton_inj line 176
  31. theorem OAI.WitnessedSeparation.Hereditary.map_singleton line 178
  32. theorem OAI.WitnessedSeparation.Hereditary.map_double line 180
  33. theorem OAI.WitnessedSeparation.Hereditary.map_pair line 186
  34. theorem OAI.WitnessedSeparation.Hereditary.pair_injective line 188
  35. theorem OAI.WitnessedSeparation.Hereditary.pair_eq_pair line 209
  36. theorem OAI.WitnessedSeparation.Hereditary.ordinal_isSet line 212
  37. theorem OAI.WitnessedSeparation.Hereditary.mem_ordinal line 214
  38. theorem OAI.WitnessedSeparation.Hereditary.ordinal_injective line 231
  39. theorem OAI.WitnessedSeparation.Hereditary.map_ordinal line 242
  40. def OAI.WitnessedSeparation.Hereditary.wrappers line 252
  41. theorem OAI.WitnessedSeparation.Hereditary.wrappers_card_le line 254
  42. theorem OAI.WitnessedSeparation.Hereditary.wrappers_trans line 257
  43. example OAI.WitnessedSeparation.(example at line 273) line 273
  44. lemma OAI.WitnessedSeparation.Hereditary.mem_closure_self line 287
  45. lemma OAI.WitnessedSeparation.Hereditary.closure_member_subset line 289
  46. lemma OAI.WitnessedSeparation.Hereditary.mem_closure_iff line 295
  47. lemma OAI.WitnessedSeparation.Hereditary.closure_transitive line 311