`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeCongrOfBalancedChoiceFree`

IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/Grow/SignedOrbitLeCongrOfBalancedChoiceFree.lean · 20 lines · 1 declarations

show as: view math explainer →

open module explainer GitHub source

Explainer status: pending

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit
   5import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeCongrRightOfBalancedChoiceFree
   6import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeCongrLeftOfBalancedChoiceFree
   7
   8namespace IndisputableMonolith.PRCGrow.SignedOrbitLeCongrOfBalancedChoiceFree
   9
  10open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  11open IndisputableMonolith.PRCGrow.SignedOrbitLeCongrRightOfBalancedChoiceFree
  12open IndisputableMonolith.PRCGrow.SignedOrbitLeCongrLeftOfBalancedChoiceFree
  13
  14theorem le_congr_of_balanced_cf {a a' b b' : SignedOrbit}
  15    (ha : SignedOrbit.balanced a a') (hb : SignedOrbit.balanced b b') :
  16    SignedOrbit.le a b ↔ SignedOrbit.le a' b' :=
  17  (le_congr_left_of_balanced_cf ha).trans (le_congr_right_of_balanced_cf hb)
  18
  19end IndisputableMonolith.PRCGrow.SignedOrbitLeCongrOfBalancedChoiceFree
  20

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