OAI/Combinatorics/TriangleRemoval/Process/WitnessDimensionEquiv.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpTerminalLeave.witnessDimensionEquiv line 18
2. lemma OAI.SharpTerminalLeave.witness_dimensions_sum line 29
3. lemma OAI.SharpTerminalLeave.finite_exp_series_le line 35
4. theorem OAI.SharpTerminalLeave.witness_dimensions_weight_sum line 39