OAI/Combinatorics/EditApproximation/Refinement/ComputedEarlierHistory.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A query gathers only its preceding history, rather than allocating the full time range used to bound that history's cardinality.

  1. theorem OAI.EditApproximation.wideEarlierInputCover_mono_history line 10
  2. theorem OAI.EditApproximation.computed_queryEarlierHistory_card line 21