OAI/SetTheory/PartitionPrinciple/Forcing/RowNames.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.Rows.namePresentation line 12
  2. def OAI.PartitionPilot.Forcing.Rows.posetAction line 14
  3. def OAI.PartitionPilot.Forcing.Rows.columnCode line 19
  4. theorem OAI.PartitionPilot.Forcing.Rows.columnCode_injective line 21
  5. def OAI.PartitionPilot.Forcing.Rows.rowName line 25
  6. theorem OAI.PartitionPilot.Forcing.Rows.entry_rowName line 31
  7. theorem OAI.PartitionPilot.Forcing.Rows.rowName_action line 41
  8. theorem OAI.PartitionPilot.Forcing.Rows.rowName_supported line 63
  9. theorem OAI.PartitionPilot.Forcing.Rows.rowName_hs line 71
  10. theorem OAI.PartitionPilot.Forcing.Rows.mem_eval_rowName line 78
  11. theorem OAI.PartitionPilot.Forcing.Rows.column_mem_eval_rowName line 92
  12. theorem OAI.PartitionPilot.Forcing.Rows.rowName_recovers_row line 103
  13. theorem OAI.PartitionPilot.Forcing.Rows.rowName_values_injective line 108