Commit 2023-06-26 14:46 d2f4ea7a

View on Github →

feat: port SetTheory.Game.Ordinal (#5480)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Game/Ordinal.lean

added theorem Ordinal.one_toPGame_leftMoves_default_eq

added theorem Ordinal.one_toPGame_moveLeft

added theorem Ordinal.toLeftMovesToPGame_symm_lt

added theorem Ordinal.toPGame_add

added theorem Ordinal.toPGame_add_mk'

added theorem Ordinal.toPGame_def

added theorem Ordinal.toPGame_eq_iff

added theorem Ordinal.toPGame_equiv_iff

added theorem Ordinal.toPGame_injective

added theorem Ordinal.toPGame_le

added theorem Ordinal.toPGame_le_iff

added theorem Ordinal.toPGame_leftMoves

added theorem Ordinal.toPGame_lf

added theorem Ordinal.toPGame_lf_iff

added theorem Ordinal.toPGame_lt

added theorem Ordinal.toPGame_lt_iff

added theorem Ordinal.toPGame_moveLeft'

added theorem Ordinal.toPGame_moveLeft

added theorem Ordinal.toPGame_moveLeft_hEq

added theorem Ordinal.toPGame_nonneg

added theorem Ordinal.toPGame_rightMoves

added theorem Ordinal.to_leftMoves_one_toPGame_symm