OAI/Geometry/CAT0Fillings/Currents/Atoms.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.atomCurrent line 35
2. lemma OAI.CAT0Fillings.atomCurrent_apply line 39
3. lemma OAI.CAT0Fillings.atomCurrent_controls line 43
4. lemma OAI.CAT0Fillings.finite_atom_measure line 50
5. lemma OAI.CAT0Fillings.atomCurrent_isMetricCurrent line 56
6. lemma OAI.CAT0Fillings.mass_atomCurrent line 71
7. lemma OAI.CAT0Fillings.IntegerChart.zero_action line 84
8. lemma OAI.CAT0Fillings.IntegerChart.zero_action_eq_zero line 96
9. lemma OAI.CAT0Fillings.IntegerChart.zero_exists_atom line 106