`IndisputableMonolith.Gravity.Analysis.Q3PatchSeatingAudit`

IndisputableMonolith/Gravity/Analysis/Q3PatchSeatingAudit.lean · 17 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.Q3PatchSeating
   2
   3/-!
   4Axiom audit for Q3PatchSeating.
   5-/
   6
   7open IndisputableMonolith.Gravity.Analysis.Q3PatchSeating
   8
   9#print axioms unseat_seat
  10#print axioms seat_unseat
  11#print axioms seat_injective
  12#print axioms seat_surjective
  13#print axioms seat_bijective
  14#print axioms seat_flipTime
  15#print axioms flipTime_involutive
  16#print axioms timeSlice_is_patch_symmetry
  17

source mirrored from github.com/jonwashburn/shape-of-logic