OAI/Analysis/SegmentLenses/Main.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SegmentLenses.midpoint_lens_main line 7

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

   Statement uses: And, Finset, OAI.SegmentLenses.ForestVertex, OAI.SegmentLenses.Ancestral, OAI.SegmentLenses.ForestAncestor, OAI.SegmentLenses.X, Eq, OAI.SegmentLenses.head, Real, LE.le, OfNat.ofNat, Norm.norm, OAI.SegmentLenses.Primal, OAI.SegmentLenses.Test, RingHom.id, HAdd.hAdd, HSub.hSub, OAI.SegmentLenses.FullDual, OAI.SegmentLenses.tail, HMul.hMul and 10 more

   Proof uses: And.intro, OAI.SegmentLenses.forest_main_tail, OAI.SegmentLenses.infinite_main_tail

   188 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: ComparatorChallenges/MidpointLenses.lean:328 (same statement text; different proof or body). Qualify references as OAI.SegmentLenses.midpoint_lens_main@path.