OAI/Combinatorics/TriangleRemoval/Process/HistoryAdditive.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpTerminalLeave.historyAdditive line 17
2. lemma OAI.SharpTerminalLeave.historyAdditive_update line 21
3. lemma OAI.SharpTerminalLeave.historyAdditive_zero line 35
4. lemma OAI.SharpTerminalLeave.historyAdditive_frozen line 39
5. theorem OAI.SharpTerminalLeave.history_additive_freedman line 44
6. lemma OAI.SharpTerminalLeave.historyAdditive_past line 98
7. theorem OAI.SharpTerminalLeave.history_additive_freedman_maximal line 114