Documentation Verification Report

Birthday

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

Statistics

Metric	Count
Definitions `birthday`, `birthday`	2
Theorems `birthday_add_le`, `birthday_eq_pGameBirthday`, `birthday_eq_zero`, `birthday_natCast`, `birthday_neg`, `birthday_ofNat`, `birthday_one`, `birthday_ordinalToGame`, `birthday_quot_le_pGameBirthday`, `birthday_star`, `birthday_sub_le`, `birthday_zero`, `le_birthday`, `neg_birthday_le`, `small_setOf_birthday_lt`, `birthday_congr`, `birthday_add`, `birthday_def`, `birthday_eq_zero`, `birthday_moveLeft_lt`, `birthday_moveRight_lt`, `birthday_natCast`, `birthday_neg`, `birthday_one`, `birthday_ordinalToPGame`, `birthday_star`, `birthday_sub`, `birthday_zero`, `le_birthday`, `lt_birthday_iff`, `neg_birthday_le`	31
Total	33

SetTheory.Game

Definitions

Name	Category	Theorems
`birthday` 📖	CompOp	15 math math: `birthday_add_le`, `birthday_neg`, `birthday_sub_le`, `birthday_natCast`, `birthday_eq_pGameBirthday`, `birthday_zero`, `birthday_one`, `birthday_ordinalToGame`, `le_birthday`, `birthday_eq_zero`, `birthday_ofNat`, `small_setOf_birthday_lt`, `neg_birthday_le`, `birthday_star`, `birthday_quot_le_pGameBirthday`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`birthday_add_le` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `birthday` `SetTheory.Game` `instAdd` `Ordinal.nadd`	—	`birthday_eq_pGameBirthday` `SetTheory.PGame.birthday_add` `birthday_quot_le_pGameBirthday`
`birthday_eq_pGameBirthday` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.birthday` `birthday`	—	`csInf_mem` `Ordinal.wellFoundedLT` `Set.image_nonempty` `Quotient.out_eq`
`birthday_eq_zero` 📖	mathematical	—	`birthday` `Ordinal` `Ordinal.zero` `SetTheory.Game` `instZero`	—	`birthday_eq_pGameBirthday` `SetTheory.PGame.game_eq` `SetTheory.PGame.Equiv.isEmpty` `SetTheory.PGame.birthday_eq_zero` `birthday_zero`
`birthday_natCast` 📖	mathematical	—	`birthday` `SetTheory.Game` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `instAddCommGroupWithOneGame` `Ordinal` `Ordinal.addMonoidWithOne`	—	`Ordinal.toGame_natCast` `birthday_ordinalToGame`
`birthday_neg` 📖	mathematical	—	`birthday` `SetTheory.Game` `instNeg`	—	`le_antisymm` `neg_neg`
`birthday_ofNat` 📖	mathematical	—	`birthday` `Ordinal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne`	—	`birthday_natCast`
`birthday_one` 📖	mathematical	—	`birthday` `SetTheory.Game` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `instAddCommGroupWithOneGame` `Ordinal` `Ordinal.one`	—	`Nat.cast_one` `birthday_natCast`
`birthday_ordinalToGame` 📖	mathematical	—	`birthday` `DFunLike.coe` `OrderEmbedding` `Ordinal` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instPartialOrderGame` `instFunLikeOrderEmbedding` `Ordinal.toGame`	—	`le_antisymm` `SetTheory.PGame.birthday_ordinalToPGame` `birthday_quot_le_pGameBirthday` `birthday_eq_pGameBirthday` `Ordinal.toPGame_le_iff` `LE.le.trans` `SetTheory.PGame.equiv_iff_game_eq` `Ordinal.mk_toPGame` `SetTheory.PGame.le_birthday`
`birthday_quot_le_pGameBirthday` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `birthday` `SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.birthday`	—	`csInf_le'`
`birthday_star` 📖	mathematical	—	`birthday` `SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.star` `Ordinal` `Ordinal.one`	—	`le_antisymm` `SetTheory.PGame.birthday_star` `birthday_quot_le_pGameBirthday` `Ordinal.one_le_iff_ne_zero` `birthday_eq_zero` `zero_def` `SetTheory.PGame.equiv_iff_game_eq` `SetTheory.PGame.Fuzzy.not_equiv` `SetTheory.PGame.star_fuzzy_zero`
`birthday_sub_le` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `birthday` `SetTheory.Game` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `instAddCommGroupWithOneGame` `Ordinal.nadd`	—	`LE.le.trans_eq` `birthday_add_le` `birthday_neg`
`birthday_zero` 📖	mathematical	—	`birthday` `SetTheory.Game` `instZero` `Ordinal` `Ordinal.zero`	—	`nonpos_iff_eq_zero` `Ordinal.canonicallyOrderedAdd` `SetTheory.PGame.birthday_zero` `birthday_quot_le_pGameBirthday`
`le_birthday` 📖	mathematical	—	`SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderGame` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `Ordinal.toGame` `birthday`	—	`birthday_eq_pGameBirthday` `LE.le.trans` `SetTheory.PGame.le_birthday` `Ordinal.toPGame_le_iff` `le_refl`
`neg_birthday_le` 📖	mathematical	—	`SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderGame` `instNeg` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `Ordinal.toGame` `birthday`	—	`neg_le` `addLeftMono` `addRightMono` `birthday_neg` `le_birthday`
`small_setOf_birthday_lt` 📖	mathematical	—	`Small` `SetTheory.Game` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `birthday`	—	`Ordinal.induction` `small_biUnion` `Ordinal.small_Iio` `Ordinal.zero_or_succ_or_isSuccLimit` `Ordinal.canonicallyOrderedAdd` `small_empty` `Ordinal.instNoMaxOrder` `small_union` `Order.lt_succ` `small_subtype` `birthday_eq_pGameBirthday` `SetTheory.PGame.game_eq` `SetTheory.PGame.Equiv.of_exists` `Quotient.out_eq` `le_rfl` `LE.le.trans_lt` `birthday_quot_le_pGameBirthday` `SetTheory.PGame.birthday_moveLeft_lt` `Set.iUnion_congr_Prop` `Order.Iio_succ` `Equiv.symm_apply_apply` `Quotient.mk_out` `SetTheory.PGame.birthday_moveRight_lt` `small_subset` `small_range` `small_prod` `small_set` `Order.IsSuccLimit.lt_iff_exists_lt`

SetTheory.PGame

Definitions

Name	Category	Theorems
`birthday` 📖	CompOp	21 math math: `birthday_add`, `birthday_one`, `le_birthday`, `birthday_moveLeft_lt`, `birthday_sub`, `short_birthday`, `SetTheory.Game.birthday_eq_pGameBirthday`, `lt_birthday_iff`, `birthday_star`, `birthday_zero`, `birthday_half`, `birthday_def`, `birthday_eq_zero`, `birthday_ordinalToPGame`, `birthday_neg`, `Relabelling.birthday_congr`, `nim_birthday`, `birthday_moveRight_lt`, `birthday_natCast`, `SetTheory.Game.birthday_quot_le_pGameBirthday`, `neg_birthday_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`birthday_add` 📖	mathematical	—	`birthday` `SetTheory.PGame` `instAdd` `Ordinal.nadd`	—	—
`birthday_def` 📖	mathematical	—	`birthday` `Ordinal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `Ordinal.lsub` `LeftMoves` `moveLeft` `RightMoves` `moveRight`	—	`birthday.eq_1`
`birthday_eq_zero` 📖	mathematical	—	`birthday` `Ordinal` `Ordinal.zero` `IsEmpty` `LeftMoves` `RightMoves`	—	`birthday_def` `Ordinal.max_eq_zero` `Ordinal.lsub_eq_zero_iff`
`birthday_moveLeft_lt` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `birthday` `moveLeft`	—	`birthday.eq_1` `lt_max_of_lt_left` `Ordinal.lt_lsub`
`birthday_moveRight_lt` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `birthday` `moveRight`	—	`birthday.eq_1` `lt_max_of_lt_right` `Ordinal.lt_lsub`
`birthday_natCast` 📖	mathematical	—	`birthday` `SetTheory.PGame` `instNatCast` `Ordinal` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne`	—	`birthday_zero` `birthday_add` `birthday_one` `Ordinal.nadd_one` `Nat.cast_add` `Nat.cast_one`
`birthday_neg` 📖	mathematical	—	`birthday` `SetTheory.PGame` `instNeg`	—	`birthday_def` `max_comm`
`birthday_one` 📖	mathematical	—	`birthday` `SetTheory.PGame` `instOnePGame` `Ordinal` `Ordinal.one`	—	`birthday_def` `birthday_zero` `Ordinal.lsub_unique` `Ordinal.succ_zero` `Ordinal.lsub_empty` `PEmpty.instIsEmpty` `sup_of_le_left` `Ordinal.canonicallyOrderedAdd`
`birthday_ordinalToPGame` 📖	mathematical	—	`birthday` `Ordinal.toPGame`	—	`Ordinal.induction` `Ordinal.toPGame.eq_1` `birthday.eq_1` `Ordinal.lsub_empty` `PEmpty.instIsEmpty` `Ordinal.max_zero_right` `isWellOrder_lt` `wellFoundedLT_toType` `Ordinal.lsub_typein` `Ordinal.typein_lt_self`
`birthday_star` 📖	mathematical	—	`birthday` `star` `Ordinal` `Ordinal.one`	—	`birthday_def` `birthday_zero` `Ordinal.lsub_unique` `Ordinal.succ_zero` `max_self`
`birthday_sub` 📖	mathematical	—	`birthday` `SetTheory.PGame` `instSub` `Ordinal.nadd`	—	`birthday_add` `birthday_neg`
`birthday_zero` 📖	mathematical	—	`birthday` `SetTheory.PGame` `instZero` `Ordinal` `Ordinal.zero`	—	`PEmpty.instIsEmpty`
`le_birthday` 📖	mathematical	—	`SetTheory.PGame` `le` `Ordinal.toPGame` `birthday`	—	`le_def` `birthday_moveLeft_lt` `Ordinal.toPGame_moveLeft'` `Equiv.symm_apply_apply` `Ordinal.isEmpty_toPGame_rightMoves`
`lt_birthday_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `birthday` `Preorder.toLE` `moveLeft` `moveRight`	—	`birthday_def` `lt_max_iff` `Ordinal.lt_lsub_iff` `LE.le.trans_lt` `birthday_moveLeft_lt` `birthday_moveRight_lt`
`neg_birthday_le` 📖	mathematical	—	`SetTheory.PGame` `le` `instNeg` `Ordinal.toPGame` `birthday`	—	`birthday_neg` `le_birthday`

SetTheory.PGame.Relabelling

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`birthday_congr` 📖	mathematical	—	`SetTheory.PGame.birthday`	—	`SetTheory.PGame.birthday.eq_def` `Ordinal.lsub_eq_of_range_eq` `Set.ext`

---

← Back to Index