OAI/Geometry/DoublingHilbert/CompactBanach.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CompactBanach.main line 20

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Exists, Nat, NormedAddCommGroup, NormedSpace, Real, CompleteSpace, Not, FiniteDimensional, Set, And, IsCompact, OAI.CompactBanach.DoublingAtMost, OAI.CompactBanach.AdmitsBiLipschitzEmbedding

   Proof uses: Exists.intro, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HPow.hPow, OAI.CompactBanach.AmbientDoubling, Subtype, PreLp, Membership.mem, AddSubgroup, OAI.DoublingHilbert.RealL2, ENNReal, OAI.DoublingHilbert.constructedSet, Iff.mp, OAI.CompactBanach.doubling_iff_ambient, LT.lt, OAI.DoublingHilbert.constructedSet_cover, Finset, LE.le, Finset.card and 139 more

   147 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: ComparatorChallenges/CompactBanach.lean:25 (same statement text; different proof or body). Qualify references as OAI.CompactBanach.main@path.

   Tactic trace: 55 steps

   Open to load the checked before-and-after goal states.