OAI/ModelTheory/Choiceless/Definability.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CPTSeparation.Operational.member_count_iff line 30
  2. lemma OAI.CPTSeparation.Operational.uniform_double_value line 53
  3. lemma OAI.CPTSeparation.Operational.uniform_singleton_value line 70
  4. lemma OAI.CPTSeparation.Operational.uniform_atoms line 87
  5. lemma OAI.CPTSeparation.Operational.uniform_union line 124
  6. lemma OAI.CPTSeparation.Operational.uniform_unique line 171
  7. def OAI.CPTSeparation.Operational.BoundedCard line 225
  8. lemma OAI.CPTSeparation.Operational.uniform_card line 229
  9. lemma OAI.CPTSeparation.Operational.uniform_boolean line 260
  10. lemma OAI.CPTSeparation.Counting.UniformDefinable.forall_finset line 290
  11. lemma OAI.CPTSeparation.Counting.UniformDefinable.forall_finite line 296
  12. lemma OAI.CPTSeparation.Counting.UniformDefinable.append_cons line 301
  13. lemma OAI.CPTSeparation.Counting.UniformDefinable.exists_vec line 307
  14. lemma OAI.CPTSeparation.Counting.UniformDefinable.compose_unary line 334
  15. lemma OAI.CPTSeparation.Counting.UniformDefinable.compose_binary line 350
  16. lemma OAI.CPTSeparation.Counting.UniformDefinable.compose_vec line 373
  17. def OAI.CPTSeparation.Operational.Term.Graph line 411
  18. lemma OAI.CPTSeparation.Operational.Term.graph_sound line 441
  19. lemma OAI.CPTSeparation.Operational.Term.eval_mem_trace line 498
  20. lemma OAI.CPTSeparation.Operational.Term.graph_complete line 503
  21. lemma OAI.CPTSeparation.Operational.uniform_comprehension line 625
  22. def OAI.CPTSeparation.Operational.Term.width line 665
  23. lemma OAI.CPTSeparation.Operational.Term.uniform_graph line 695
  24. def OAI.CPTSeparation.Operational.Rule.trace line 822
  25. def OAI.CPTSeparation.Operational.Rule.bound line 831
  26. lemma OAI.CPTSeparation.Operational.Rule.closure_update_subset_trace line 839
  27. lemma OAI.CPTSeparation.Operational.Rule.card_trace_le line 876
  28. def OAI.CPTSeparation.Operational.Rule.Graph line 922
  29. lemma OAI.CPTSeparation.Operational.Rule.graph_sound line 938
  30. lemma OAI.CPTSeparation.Operational.Rule.graph_complete line 977
  31. def OAI.CPTSeparation.Operational.Rule.width line 1041
  32. lemma OAI.CPTSeparation.Operational.Rule.uniform_graph line 1070