Ordinal

📁 Source: Mathlib/SetTheory/Game/Ordinal.lean

Statistics

Metric	Count
Definitions `oneToPGameRelabelling`, `toGame`, `toLeftMovesToPGame`, `toPGame`, `toPGameEmbedding`, `uniqueOneToPGameLeftMoves`, `zeroToPGameRelabelling`	7
Theorems `isEmpty_toPGame_rightMoves`, `isEmpty_zero_toPGame_leftMoves`, `mk_toPGame`, `one_toPGame_leftMoves_default_eq`, `one_toPGame_moveLeft`, `toGame_inj`, `toGame_injective`, `toGame_le_iff`, `toGame_lf_iff`, `toGame_lt_iff`, `toGame_nadd`, `toGame_natCast`, `toGame_nmul`, `toGame_one`, `toGame_zero`, `toLeftMovesToPGame_symm_lt`, `toPGameEmbedding_apply`, `toPGame_equiv_iff`, `toPGame_inj`, `toPGame_injective`, `toPGame_le`, `toPGame_le_iff`, `toPGame_leftMoves`, `toPGame_lf`, `toPGame_lf_iff`, `toPGame_lt`, `toPGame_lt_iff`, `toPGame_moveLeft`, `toPGame_moveLeft'`, `toPGame_moveLeft_hEq`, `toPGame_nadd`, `toPGame_natCast`, `toPGame_nmul`, `toPGame_nonneg`, `toPGame_one`, `toPGame_rightMoves`, `toPGame_zero`, `to_leftMoves_one_toPGame_symm`	38
Total	45

Ordinal

Definitions

Name	Category	Theorems
`oneToPGameRelabelling` 📖	CompOp	—
`toGame` 📖	CompOp	14 math math: `toGame_lt_iff`, `toGame_one`, `SetTheory.Game.birthday_ordinalToGame`, `SetTheory.Game.le_birthday`, `mk_toPGame`, `toGame_zero`, `toGame_nmul`, `toGame_lf_iff`, `toGame_inj`, `SetTheory.Game.neg_birthday_le`, `toGame_injective`, `toGame_nadd`, `toGame_natCast`, `toGame_le_iff`
`toLeftMovesToPGame` 📖	CompOp	5 math math: `one_toPGame_leftMoves_default_eq`, `toPGame_moveLeft`, `to_leftMoves_one_toPGame_symm`, `toLeftMovesToPGame_symm_lt`, `toPGame_moveLeft'`
`toPGame` 📖	CompOp	33 math math: `toPGame_lf_iff`, `isEmpty_toPGame_rightMoves`, `SetTheory.PGame.le_birthday`, `one_toPGame_leftMoves_default_eq`, `toPGame_zero`, `toPGame_rightMoves`, `toPGame_nmul`, `isEmpty_zero_toPGame_leftMoves`, `toPGame_one`, `SetTheory.PGame.numeric_toPGame`, `toPGame_lf`, `toPGame_inj`, `one_toPGame_moveLeft`, `toPGame_nonneg`, `mk_toPGame`, `toPGame_le`, `toPGame_natCast`, `SetTheory.PGame.birthday_ordinalToPGame`, `toGame_nmul`, `toPGame_leftMoves`, `toPGame_lt_iff`, `toPGame_moveLeft`, `toPGame_moveLeft_hEq`, `toPGame_nadd`, `to_leftMoves_one_toPGame_symm`, `toPGame_injective`, `toPGame_le_iff`, `toLeftMovesToPGame_symm_lt`, `toPGame_lt`, `toPGameEmbedding_apply`, `toPGame_equiv_iff`, `SetTheory.PGame.neg_birthday_le`, `toPGame_moveLeft'`
`toPGameEmbedding` 📖	CompOp	1 math math: `toPGameEmbedding_apply`
`uniqueOneToPGameLeftMoves` 📖	CompOp	1 math math: `one_toPGame_leftMoves_default_eq`
`zeroToPGameRelabelling` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmpty_toPGame_rightMoves` 📖	mathematical	—	`IsEmpty` `SetTheory.PGame.RightMoves` `toPGame`	—	`toPGame_rightMoves` `PEmpty.instIsEmpty`
`isEmpty_zero_toPGame_leftMoves` 📖	mathematical	—	`IsEmpty` `SetTheory.PGame.LeftMoves` `toPGame` `Ordinal` `zero`	—	`toPGame_leftMoves` `isEmpty_toType_zero`
`mk_toPGame` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `toPGame` `DFunLike.coe` `OrderEmbedding` `Ordinal` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `instFunLikeOrderEmbedding` `toGame`	—	—
`one_toPGame_leftMoves_default_eq` 📖	mathematical	—	`SetTheory.PGame.LeftMoves` `toPGame` `Ordinal` `one` `Unique.instInhabited` `uniqueOneToPGameLeftMoves` `DFunLike.coe` `Equiv` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `partialOrder` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLeftMovesToPGame` `Set` `Set.instMembership` `zero` `Preorder.toLT` `Set.mem_Iio` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne`	—	—
`one_toPGame_moveLeft` 📖	mathematical	—	`SetTheory.PGame.moveLeft` `toPGame` `Ordinal` `one` `zero`	—	`toPGame_moveLeft'` `Set.mem_Iio` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne` `to_leftMoves_one_toPGame_symm`
`toGame_inj` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `instFunLikeOrderEmbedding` `toGame`	—	—
`toGame_injective` 📖	mathematical	—	`Ordinal` `SetTheory.Game` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `instFunLikeOrderEmbedding` `toGame`	—	`RelEmbedding.injective`
`toGame_le_iff` 📖	mathematical	—	`SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `SetTheory.Game.instPartialOrderGame` `DFunLike.coe` `OrderEmbedding` `Ordinal` `partialOrder` `instFunLikeOrderEmbedding` `toGame`	—	`toPGame_le_iff`
`toGame_lf_iff` 📖	mathematical	—	`SetTheory.Game.LF` `DFunLike.coe` `OrderEmbedding` `Ordinal` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `instFunLikeOrderEmbedding` `toGame` `Preorder.toLT`	—	`toPGame_lf_iff`
`toGame_lt_iff` 📖	mathematical	—	`SetTheory.Game` `Preorder.toLT` `PartialOrder.toPreorder` `SetTheory.Game.instPartialOrderGame` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `partialOrder` `instFunLikeOrderEmbedding` `toGame`	—	`toPGame_lt_iff`
`toGame_nadd` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `instFunLikeOrderEmbedding` `toGame` `nadd` `SetTheory.Game.instAdd`	—	`SetTheory.PGame.game_eq` `toPGame_nadd`
`toGame_natCast` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `instFunLikeOrderEmbedding` `toGame` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `SetTheory.Game.instAddCommGroupWithOneGame`	—	`SetTheory.PGame.Relabelling.equiv` `Nat.cast_add` `nadd_nat` `toGame_nadd` `Nat.cast_one`
`toGame_nmul` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `instFunLikeOrderEmbedding` `toGame` `nmul` `SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instMul` `toPGame`	—	`SetTheory.PGame.game_eq` `toPGame_nmul`
`toGame_one` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `instFunLikeOrderEmbedding` `toGame` `one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `SetTheory.Game.instAddCommGroupWithOneGame`	—	`SetTheory.PGame.game_eq` `toPGame_one`
`toGame_zero` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `instFunLikeOrderEmbedding` `toGame` `zero` `SetTheory.Game.instZero`	—	`SetTheory.PGame.game_eq` `toPGame_zero`
`toLeftMovesToPGame_symm_lt` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Set` `Set.instMembership` `Set.Iio` `DFunLike.coe` `Equiv` `SetTheory.PGame.LeftMoves` `toPGame` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toLeftMovesToPGame`	—	`Subtype.prop`
`toPGameEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Ordinal` `SetTheory.PGame` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetTheory.PGame.le` `RelEmbedding.instFunLike` `toPGameEmbedding` `toPGame`	—	—
`toPGame_equiv_iff` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `toPGame`	—	`le_antisymm_iff` `toPGame_le_iff`
`toPGame_inj` 📖	mathematical	—	`toPGame`	—	`toPGame_injective`
`toPGame_injective` 📖	mathematical	—	`Ordinal` `SetTheory.PGame` `toPGame`	—	`toPGame_equiv_iff` `SetTheory.PGame.equiv_of_eq`
`toPGame_le` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`SetTheory.PGame` `SetTheory.PGame.le` `toPGame`	—	`SetTheory.PGame.le_iff_forall_lf` `toPGame_moveLeft'` `toPGame_lf` `LT.lt.trans_le` `toLeftMovesToPGame_symm_lt` `isEmpty_toPGame_rightMoves`
`toPGame_le_iff` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.le` `toPGame` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `not_le` `SetTheory.PGame.not_le` `toPGame_lf` `toPGame_le`
`toPGame_leftMoves` 📖	mathematical	—	`SetTheory.PGame.LeftMoves` `toPGame` `ToType`	—	`toPGame.eq_1` `SetTheory.PGame.LeftMoves.eq_1`
`toPGame_lf` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`SetTheory.PGame.LF` `toPGame`	—	`toPGame_moveLeft` `SetTheory.PGame.moveLeft_lf`
`toPGame_lf_iff` 📖	mathematical	—	`SetTheory.PGame.LF` `toPGame` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `not_lt` `SetTheory.PGame.not_lf` `toPGame_le` `toPGame_lf`
`toPGame_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`SetTheory.PGame` `SetTheory.PGame.instPreorder` `toPGame`	—	`toPGame_le` `LT.lt.le` `toPGame_lf`
`toPGame_lt_iff` 📖	mathematical	—	`SetTheory.PGame` `Preorder.toLT` `SetTheory.PGame.instPreorder` `toPGame` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `not_lt` `not_lt_of_ge` `toPGame_le` `toPGame_lt`
`toPGame_moveLeft` 📖	mathematical	—	`SetTheory.PGame.moveLeft` `toPGame` `DFunLike.coe` `Equiv` `Set.Elem` `Ordinal` `Set.Iio` `PartialOrder.toPreorder` `partialOrder` `SetTheory.PGame.LeftMoves` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLeftMovesToPGame` `Set` `Set.instMembership`	—	`toPGame_moveLeft'` `Equiv.symm_apply_apply`
`toPGame_moveLeft'` 📖	mathematical	—	`SetTheory.PGame.moveLeft` `toPGame` `Ordinal` `Set` `Set.instMembership` `Set.Iio` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `Equiv` `SetTheory.PGame.LeftMoves` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toLeftMovesToPGame`	—	`congr_heq` `toPGame_moveLeft_hEq`
`toPGame_moveLeft_hEq` 📖	mathematical	—	`SetTheory.PGame.moveLeft` `toPGame` `Ordinal` `Set` `Set.instMembership` `Set.Iio` `PartialOrder.toPreorder` `partialOrder` `ToType.toOrd`	—	`toPGame.eq_1`
`toPGame_nadd` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `toPGame` `nadd` `SetTheory.PGame.instAdd`	—	—
`toPGame_natCast` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `toPGame` `Ordinal` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `SetTheory.PGame.instNatCast`	—	`SetTheory.PGame.equiv_iff_game_eq` `mk_toPGame` `toGame_natCast` `SetTheory.PGame.quot_natCast`
`toPGame_nmul` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `toPGame` `nmul` `SetTheory.PGame.instMul`	—	—
`toPGame_nonneg` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.le` `SetTheory.PGame.instZero` `toPGame`	—	`LE.le.trans` `SetTheory.PGame.Relabelling.ge` `toPGame_le` `zero_le` `canonicallyOrderedAdd`
`toPGame_one` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `toPGame` `Ordinal` `one` `SetTheory.PGame.instOnePGame`	—	`SetTheory.PGame.Relabelling.equiv`
`toPGame_rightMoves` 📖	mathematical	—	`SetTheory.PGame.RightMoves` `toPGame`	—	`toPGame.eq_1` `SetTheory.PGame.RightMoves.eq_1`
`toPGame_zero` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `toPGame` `Ordinal` `zero` `SetTheory.PGame.instZero`	—	`SetTheory.PGame.Relabelling.equiv`
`to_leftMoves_one_toPGame_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SetTheory.PGame.LeftMoves` `toPGame` `Ordinal` `one` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `partialOrder` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toLeftMovesToPGame` `Set` `Set.instMembership` `zero` `Preorder.toLT` `Set.mem_Iio` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne`	—	`Set.mem_Iio` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne` `Unique.instSubsingleton`

---

← Back to Index