OAI/Combinatorics/TriangleRemoval/Stability/MovingResidualForcing.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpTerminalLeave.moving_active_subsetline 14 - lemma
OAI.SharpTerminalLeave.activeLinf_monoline 21 - def
OAI.SharpTerminalLeave.movingResidualForcingline 25 - lemma
OAI.SharpTerminalLeave.movingResidualForcing_zeroline 35 - lemma
OAI.SharpTerminalLeave.movingResidualForcing_succline 39 - lemma
OAI.SharpTerminalLeave.movingResidualForcing_boundline 44 - lemma
OAI.SharpTerminalLeave.movingStar_actual_responseline 74 - theorem
OAI.SharpTerminalLeave.movingStar_mixed_stabilityline 115