OAI/Combinatorics/Progressions/Estimates/ComparableScalarPhysicalFamilyPatch.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.comparableScalarSlice_early_room line 11
  2. theorem OAI.Erdos3.comparableScalarSlice_extra_caps line 24
  3. theorem OAI.Erdos3.comparableScalarSlice_long_scale line 61
  4. theorem OAI.Erdos3.exists_indexed_comparableScalarSliceGeometryTransfer line 84
  5. def OAI.Erdos3.ComparableUnconditionedScalarSliceTransferStatement line 204
  6. theorem OAI.Erdos3.exists_comparable_unconditioned_scalar_slice_transfer line 248
  7. def OAI.Erdos3.IndexedComparableUnconditionedScalarSliceTransferStatement line 329
  8. theorem OAI.Erdos3.exists_indexed_comparable_unconditioned_scalar_slice_transfer line 374
  9. def OAI.Erdos3.ComparableScalarSharedSliceTailStatement line 457
  10. theorem OAI.Erdos3.exists_comparable_scalar_shared_slice_tail line 502
  11. theorem OAI.Erdos3.exists_comparable_scalar_retained_slice_patch line 537
  12. theorem OAI.Erdos3.exists_comparable_scalar_early_retained_slice_patch line 673
  13. theorem OAI.Erdos3.exists_comparable_scalar_physical_family_patch line 772