OAI/Combinatorics/VariableWL/BlockExtensions.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Blocks.SupportConnected line 11
  2. def OAI.VariableWL.Blocks.NoReal line 15
  3. def OAI.VariableWL.Blocks.Avoids line 18
  4. theorem OAI.VariableWL.Blocks.supportLinks_mono line 21
  5. theorem OAI.VariableWL.Blocks.supportTypes_mono line 26
  6. theorem OAI.VariableWL.Blocks.avoids_mono line 31
  7. theorem OAI.VariableWL.Blocks.supportTypes_nonempty line 35
  8. theorem OAI.VariableWL.Blocks.support_noReal_reach line 41
  9. theorem OAI.VariableWL.Blocks.component_support_connected line 46
  10. theorem OAI.VariableWL.Blocks.internal_same_address line 53
  11. theorem OAI.VariableWL.Blocks.wrapping_address_allowed_superset line 72
  12. def OAI.VariableWL.Blocks.AddressCondition line 92
  13. def OAI.VariableWL.Blocks.Admissible line 98
  14. theorem OAI.VariableWL.Blocks.addressAt_real line 104
  15. theorem OAI.VariableWL.Blocks.admissible_of_one line 107
  16. theorem OAI.VariableWL.Blocks.addressCondition_exists line 119
  17. theorem OAI.VariableWL.Blocks.admissible_exists line 149
  18. theorem OAI.VariableWL.Blocks.addressAt_cut_independent_superset line 169
  19. theorem OAI.VariableWL.Blocks.admissible_cut_change line 193
  20. theorem OAI.VariableWL.Blocks.admissible_restrict line 210
  21. theorem OAI.VariableWL.Blocks.admissible_lift line 239
  22. def OAI.VariableWL.Blocks.componentMap line 306
  23. theorem OAI.VariableWL.Blocks.componentMap_mk line 311
  24. theorem OAI.VariableWL.Blocks.componentBlocks_map_subset line 316
  25. theorem OAI.VariableWL.Blocks.wrapping_component_all line 326
  26. theorem OAI.VariableWL.Blocks.wrapping_component_unique line 336
  27. theorem OAI.VariableWL.Blocks.vectorShift_agree line 349
  28. theorem OAI.VariableWL.Blocks.potentialValues_shift_agree line 355
  29. theorem OAI.VariableWL.Blocks.potentialValues_potentials_agree line 365
  30. theorem OAI.VariableWL.Blocks.readout_type_mem line 373
  31. abbrev OAI.VariableWL.Blocks.ReadoutValues line 382
  32. def OAI.VariableWL.Blocks.OffsetFamily line 384
  33. def OAI.VariableWL.Blocks.representedValues line 394
  34. theorem OAI.VariableWL.Blocks.representedValues_on_block line 400
  35. theorem OAI.VariableWL.Blocks.offsetFamily_nonempty line 410