OAI/Analysis/LipschitzEquivalence/Model.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LipschitzCounterexample.RealL2 line 10

   Also declared: ComparatorChallenges/LipschitzEquivalence.lean:10 (same declaration text).

2. abbrev OAI.LipschitzCounterexample.C0L2 line 11

   Also declared: ComparatorChallenges/LipschitzEquivalence.lean:11 (same declaration text).

3. structure OAI.LipschitzCounterexample.SeparableRealBanach line 13

   Also declared: ComparatorChallenges/LipschitzEquivalence.lean:13 (same declaration text).

4. def OAI.LipschitzCounterexample.ContainsLinearCopy line 24

   Also declared: ComparatorChallenges/LipschitzEquivalence.lean:24 (same declaration text).

5. def OAI.LipschitzCounterexample.MainClaim line 28

   Also declared: ComparatorChallenges/LipschitzEquivalence.lean:28 (same declaration text).