Commit 2024-11-18 22:39 db980d62

View on Github →

feat: define PGame.identical PGame.memₗ PGame.memᵣ (#17122)

Estimated changes

Modified Mathlib/SetTheory/Game/PGame.lean

added theorem SetTheory.PGame.Identical.congr_left

added theorem SetTheory.PGame.Identical.congr_right

added theorem SetTheory.PGame.Identical.equiv

added theorem SetTheory.PGame.Identical.ext

added theorem SetTheory.PGame.Identical.ext_iff

added theorem SetTheory.PGame.Identical.ge

added theorem SetTheory.PGame.Identical.le

added theorem SetTheory.PGame.Identical.moveLeft

added theorem SetTheory.PGame.Identical.moveRight

added theorem SetTheory.PGame.Identical.of_equiv

added theorem SetTheory.PGame.Identical.of_fn

added def SetTheory.PGame.Identical

added def SetTheory.PGame.identicalSetoid

added theorem SetTheory.PGame.identical_comm

added theorem SetTheory.PGame.identical_iff'

added theorem SetTheory.PGame.identical_iff

added theorem SetTheory.PGame.identical_of_isEmpty

added theorem SetTheory.PGame.memᵣ.congr_left

added theorem SetTheory.PGame.memᵣ.congr_right

added def SetTheory.PGame.memᵣ

added theorem SetTheory.PGame.memᵣ_def

added theorem SetTheory.PGame.memₗ.congr_left

added theorem SetTheory.PGame.memₗ.congr_right

added def SetTheory.PGame.memₗ

added theorem SetTheory.PGame.memₗ_def

added theorem SetTheory.PGame.moveLeft_memₗ

added theorem SetTheory.PGame.moveRight_memᵣ