OAI/Analysis/LipschitzEquivalence/FiniteRows.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.LipschitzCounterexample.CompactWSC.RowFamilyline 11 - def
OAI.LipschitzCounterexample.CompactWSC.RowFamily.Richline 19 - def
OAI.LipschitzCounterexample.CompactWSC.RowFamily.restrictline 21 - theorem
OAI.LipschitzCounterexample.CompactWSC.RowFamily.rich_monochromaticline 25 - theorem
OAI.LipschitzCounterexample.CompactWSC.RowFamily.rich_finite_coverline 51