Basic

📁 Source: Mathlib/SetTheory/Nimber/Basic.lean

Statistics

Metric	Count
Definitions Nimber, add, instAdd, instAddCommGroupWithOne, instConditionallyCompleteLinearOrderBot, instLinearOrder, instNeg, instOrderBot, instSuccOrder, rec, toOrdinal, «term∗_», toNimber, instInhabitedNimber, instNontrivialNimber, instOneNimber, instWellFoundedRelationNimber, instZeroNimber	18
Theorems add_assoc, add_cancel_left, add_cancel_right, add_comm, add_def, add_eq_zero, add_le_of_forall_ne, add_nat, add_ne_zero_iff, add_self, add_trichotomy, add_zero, bot_eq_zero, eq_nat_of_le_nat, exists_of_lt_add, induction, instIsLeftCancelAdd, instIsRightCancelAdd, instNeZeroOne, instNoMaxOrder, instWellFoundedLT, instZeroLEOneClass, le_zero, lt_add_cases, lt_one_iff_zero, lt_wf, neg_eq, not_bddAbove_compl_of_small, not_lt_zero, one_le_iff_ne_zero, pos_iff_ne_zero, small_Icc, small_Ico, small_Iic, small_Iio, small_Ioc, small_Ioo, succ_def, toOrdinal_eq_one, toOrdinal_eq_zero, toOrdinal_max, toOrdinal_min, toOrdinal_one, toOrdinal_symm_eq, toOrdinal_toNimber, toOrdinal_zero, uncountable, zero_add, toNimber_eq_one, toNimber_eq_zero, toNimber_max, toNimber_min, toNimber_one, toNimber_symm_eq, toNimber_toOrdinal, toNimber_zero, not_small_nimber	57
Total	75

Nimber

Definitions

Name	Category	Theorems
add 📖	CompOp	—
instAdd 📖	CompOp	22 math math: SetTheory.PGame.grundyValue_nim_add_nim, add_le_of_forall_ne, add_self, add_trichotomy, add_def, add_cancel_left, mul_add, add_cancel_right, add_nat, instIsRightCancelAdd, cons_mem_invSet, instIsLeftCancelAdd, add_eq_zero, mul_def, zero_add, add_comm, add_assoc, add_mul, add_zero, exists_of_lt_mul, SetTheory.PGame.nim_add_nim_equiv, SetTheory.PGame.grundyValue_add
instAddCommGroupWithOne 📖	CompOp	1 math math: instCharPOfNatNat
instConditionallyCompleteLinearOrderBot 📖	CompOp	26 math math: SetTheory.PGame.grundyValue_eq_sInf_moveLeft, succ_def, mul_le_of_forall_ne, Ordinal.toNimber_min, add_le_of_forall_ne, toOrdinal_max, toOrdinal_min, pos_iff_ne_zero, add_trichotomy, add_def, SetTheory.PGame.grundyValue_eq_sInf_moveRight, SetTheory.PGame.grundyValue_le_of_forall_moveLeft, small_Ioo, not_bddAbove_compl_of_small, not_lt_zero, small_Ioc, small_Icc, small_Iic, one_le_iff_ne_zero, mul_def, small_Ico, Ordinal.toNimber_max, SetTheory.PGame.grundyValue_le_of_forall_moveRight, le_zero, small_Iio, lt_one_iff_zero
instLinearOrder 📖	CompOp	27 math math: Ordinal.toNimber_eq_zero, SetTheory.PGame.grundyValue_eq_iff_equiv_nim, Ordinal.toNimber_symm_eq, SetTheory.PGame.grundyValue_nim_add_nim, succ_def, Ordinal.toNimber_min, toOrdinal_max, toOrdinal_min, add_nat, instWellFoundedLT, SetTheory.PGame.equiv_nim_grundyValue, Ordinal.toNimber_one, toOrdinal_eq_one, toOrdinal_one, instZeroLEOneClass, instNoMaxOrder, lt_wf, Ordinal.toNimber_zero, Ordinal.toNimber_toOrdinal, Ordinal.toNimber_max, Ordinal.toNimber_eq_one, toOrdinal_symm_eq, SetTheory.PGame.nim_grundyValue, toOrdinal_zero, toOrdinal_toNimber, SetTheory.PGame.nim_add_nim_equiv, toOrdinal_eq_zero
instNeg 📖	CompOp	1 math math: neg_eq
instOrderBot 📖	CompOp	—
instSuccOrder 📖	CompOp	1 math math: succ_def
rec 📖	CompOp	—
toOrdinal 📖	CompOp	14 math math: SetTheory.PGame.grundyValue_eq_iff_equiv_nim, Ordinal.toNimber_symm_eq, succ_def, toOrdinal_max, toOrdinal_min, SetTheory.PGame.equiv_nim_grundyValue, toOrdinal_eq_one, toOrdinal_one, Ordinal.toNimber_toOrdinal, toOrdinal_symm_eq, toOrdinal_zero, toOrdinal_toNimber, SetTheory.PGame.nim_add_nim_equiv, toOrdinal_eq_zero
«term∗_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_assoc 📖	mathematical	—	Nimber instAdd	—	—
add_cancel_left 📖	mathematical	—	Nimber instAdd	—	add_assoc add_self zero_add
add_cancel_right 📖	mathematical	—	Nimber instAdd	—	add_assoc add_self add_zero
add_comm 📖	mathematical	—	Nimber instAdd	—	—
add_def 📖	mathematical	—	Nimber instAdd InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Compl.compl Set Set.instCompl setOf Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup	—	add.eq_1
add_eq_zero 📖	mathematical	—	Nimber instAdd instZeroNimber	—	—
add_le_of_forall_ne 📖	mathematical	—	Nimber Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instAdd	—	exists_of_lt_add
add_nat 📖	mathematical	—	Nimber instAdd DFunLike.coe OrderIso Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instFunLikeOrderIso Ordinal.toNimber AddMonoidWithOne.toNatCast Ordinal.addMonoidWithOne	—	—
add_ne_zero_iff 📖	—	—	—	—	Iff.not add_eq_zero
add_self 📖	mathematical	—	Nimber instAdd instZeroNimber	—	add_eq_zero
add_trichotomy 📖	mathematical	—	Nimber Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instAdd	—	exists_of_lt_add pos_iff_ne_zero add_eq_zero add_comm add_cancel_right
add_zero 📖	mathematical	—	Nimber instAdd instZeroNimber	—	le_antisymm add_le_of_forall_ne LT.lt.ne not_lt_zero Eq.not_lt instIsRightCancelAdd
bot_eq_zero 📖	mathematical	—	Bot.bot OrderBot.toBot Nat.instOrderBot	—	—
eq_nat_of_le_nat 📖	—	Nimber Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot DFunLike.coe OrderIso Ordinal Ordinal.partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instFunLikeOrderIso Ordinal.toNimber AddMonoidWithOne.toNatCast Ordinal.addMonoidWithOne	—	—	Ordinal.lt_omega0 LE.le.trans_lt Ordinal.nat_lt_omega0
exists_of_lt_add 📖	—	Nimber Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instAdd	—	—	notMem_of_lt_csInf' add_def Set.mem_compl_iff
induction 📖	—	—	—	—	Ordinal.induction
instIsLeftCancelAdd 📖	mathematical	—	IsLeftCancelAdd Nimber instAdd	—	le_antisymm le_of_not_gt
instIsRightCancelAdd 📖	mathematical	—	IsRightCancelAdd Nimber instAdd	—	le_antisymm le_of_not_gt
instNeZeroOne 📖	mathematical	—	Nimber instZeroNimber instOneNimber	—	Ordinal.instNeZeroOne
instNoMaxOrder 📖	mathematical	—	NoMaxOrder Nimber Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder	—	Ordinal.instNoMaxOrder
instWellFoundedLT 📖	mathematical	—	WellFoundedLT Nimber Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder	—	Ordinal.wellFoundedLT
instZeroLEOneClass 📖	mathematical	—	ZeroLEOneClass Nimber instZeroNimber instOneNimber Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder	—	Ordinal.instZeroLEOneClass
le_zero 📖	mathematical	—	Nimber Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instZeroNimber	—	nonpos_iff_eq_zero Ordinal.canonicallyOrderedAdd
lt_add_cases 📖	—	Nimber Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instAdd	—	—	add_trichotomy add_ne_zero_iff LT.lt.ne add_assoc LT.lt.asymm add_comm
lt_one_iff_zero 📖	mathematical	—	Nimber Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instOneNimber instZeroNimber	—	Ordinal.lt_one_iff_zero
lt_wf 📖	mathematical	—	Nimber Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder	—	Ordinal.lt_wf
neg_eq 📖	mathematical	—	Nimber instNeg	—	—
not_bddAbove_compl_of_small 📖	mathematical	—	BddAbove Nimber Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Compl.compl Set Set.instCompl	—	Ordinal.not_bddAbove_compl_of_small
not_lt_zero 📖	mathematical	—	Nimber Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instZeroNimber	—	not_lt_zero Ordinal.canonicallyOrderedAdd
one_le_iff_ne_zero 📖	mathematical	—	Nimber Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instOneNimber	—	Ordinal.one_le_iff_ne_zero
pos_iff_ne_zero 📖	mathematical	—	Nimber Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instZeroNimber	—	pos_iff_ne_zero Ordinal.canonicallyOrderedAdd
small_Icc 📖	mathematical	—	Small Set.Elem Nimber Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Icc
small_Ico 📖	mathematical	—	Small Set.Elem Nimber Set.Ico PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Ico
small_Iic 📖	mathematical	—	Small Set.Elem Nimber Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Iic
small_Iio 📖	mathematical	—	Small Set.Elem Nimber Set.Iio PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Iio
small_Ioc 📖	mathematical	—	Small Set.Elem Nimber Set.Ioc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Ioc
small_Ioo 📖	mathematical	—	Small Set.Elem Nimber Set.Ioo PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Ioo
succ_def 📖	mathematical	—	Order.succ Nimber PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instSuccOrder DFunLike.coe OrderIso Ordinal Preorder.toLE Ordinal.partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instFunLikeOrderIso Ordinal.toNimber Ordinal.add toOrdinal Ordinal.one	—	—
toOrdinal_eq_one 📖	mathematical	—	DFunLike.coe OrderIso Nimber Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder Ordinal.partialOrder instFunLikeOrderIso toOrdinal Ordinal.one instOneNimber	—	—
toOrdinal_eq_zero 📖	mathematical	—	DFunLike.coe OrderIso Nimber Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder Ordinal.partialOrder instFunLikeOrderIso toOrdinal Ordinal.zero instZeroNimber	—	—
toOrdinal_max 📖	mathematical	—	DFunLike.coe OrderIso Nimber Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder Ordinal.partialOrder instFunLikeOrderIso toOrdinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Ordinal.instConditionallyCompleteLinearOrderBot	—	—
toOrdinal_min 📖	mathematical	—	DFunLike.coe OrderIso Nimber Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder Ordinal.partialOrder instFunLikeOrderIso toOrdinal SemilatticeInf.toMin ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Ordinal.instConditionallyCompleteLinearOrderBot	—	—
toOrdinal_one 📖	mathematical	—	DFunLike.coe OrderIso Nimber Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder Ordinal.partialOrder instFunLikeOrderIso toOrdinal instOneNimber Ordinal.one	—	—
toOrdinal_symm_eq 📖	mathematical	—	OrderIso.symm Nimber Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder Ordinal.partialOrder toOrdinal Ordinal.toNimber	—	—
toOrdinal_toNimber 📖	mathematical	—	DFunLike.coe OrderIso Ordinal Nimber Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instFunLikeOrderIso Ordinal.toNimber toOrdinal	—	—
toOrdinal_zero 📖	mathematical	—	DFunLike.coe OrderIso Nimber Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder Ordinal.partialOrder instFunLikeOrderIso toOrdinal instZeroNimber Ordinal.zero	—	—
uncountable 📖	mathematical	—	Uncountable Nimber	—	Ordinal.uncountable
zero_add 📖	mathematical	—	Nimber instAdd instZeroNimber	—	add_comm add_zero

Ordinal

Definitions

Name	Category	Theorems
toNimber 📖	CompOp	15 math math: toNimber_eq_zero, toNimber_symm_eq, SetTheory.PGame.grundyValue_nim_add_nim, Nimber.succ_def, toNimber_min, Nimber.add_nat, toNimber_one, toNimber_zero, toNimber_toOrdinal, toNimber_max, toNimber_eq_one, Nimber.toOrdinal_symm_eq, SetTheory.PGame.nim_grundyValue, Nimber.toOrdinal_toNimber, SetTheory.PGame.nim_add_nim_equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNimber_eq_one 📖	mathematical	—	DFunLike.coe OrderIso Ordinal Nimber Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nimber.instLinearOrder instFunLikeOrderIso toNimber instOneNimber one	—	—
toNimber_eq_zero 📖	mathematical	—	DFunLike.coe OrderIso Ordinal Nimber Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nimber.instLinearOrder instFunLikeOrderIso toNimber instZeroNimber zero	—	—
toNimber_max 📖	mathematical	—	DFunLike.coe OrderIso Ordinal Nimber Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nimber.instLinearOrder instFunLikeOrderIso toNimber SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Nimber.instConditionallyCompleteLinearOrderBot	—	—
toNimber_min 📖	mathematical	—	DFunLike.coe OrderIso Ordinal Nimber Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nimber.instLinearOrder instFunLikeOrderIso toNimber SemilatticeInf.toMin ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Nimber.instConditionallyCompleteLinearOrderBot	—	—
toNimber_one 📖	mathematical	—	DFunLike.coe OrderIso Ordinal Nimber Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nimber.instLinearOrder instFunLikeOrderIso toNimber one instOneNimber	—	—
toNimber_symm_eq 📖	mathematical	—	OrderIso.symm Ordinal Nimber Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nimber.instLinearOrder toNimber Nimber.toOrdinal	—	—
toNimber_toOrdinal 📖	mathematical	—	DFunLike.coe OrderIso Nimber Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nimber.instLinearOrder partialOrder instFunLikeOrderIso Nimber.toOrdinal toNimber	—	—
toNimber_zero 📖	mathematical	—	DFunLike.coe OrderIso Ordinal Nimber Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nimber.instLinearOrder instFunLikeOrderIso toNimber zero instZeroNimber	—	—

(root)

Definitions

Name	Category	Theorems
Nimber 📖	CompOp	81 math math: Ordinal.toNimber_eq_zero, SetTheory.PGame.grundyValue_eq_sInf_moveLeft, Nimber.instSmallElemInvSet, not_small_nimber, SetTheory.PGame.grundyValue_eq_iff_equiv_nim, Ordinal.toNimber_symm_eq, SetTheory.PGame.grundyValue_nim_add_nim, Nimber.succ_def, Nimber.instNoZeroDivisors, Nimber.mul_le_of_forall_ne, Ordinal.toNimber_min, Nimber.add_le_of_forall_ne, Nimber.mul_assoc, Nimber.zero_mem_invSet, Nimber.add_self, Nimber.toOrdinal_max, Nimber.toOrdinal_min, Nimber.pos_iff_ne_zero, Nimber.add_trichotomy, Nimber.add_def, Nimber.add_cancel_left, SetTheory.PGame.grundyValue_zero, SetTheory.PGame.grundyValue_eq_sInf_moveRight, SetTheory.PGame.grundyValue_le_of_forall_moveLeft, Nimber.uncountable, Nimber.invAux_notMem_invSet, Nimber.instCharPOfNatNat, Nimber.mul_add, Nimber.add_cancel_right, Nimber.add_nat, Nimber.small_Ioo, Nimber.instIsDomain, SetTheory.PGame.grundyValue_star, Nimber.instWellFoundedLT, SetTheory.PGame.equiv_nim_grundyValue, Ordinal.toNimber_one, Nimber.instIsRightCancelAdd, Nimber.toOrdinal_eq_one, Nimber.mul_invAux_cancel, Nimber.one_mul, Nimber.instIsLeftCancelAdd, Nimber.not_bddAbove_compl_of_small, Nimber.toOrdinal_one, Nimber.instNeZeroOne, Nimber.not_lt_zero, Nimber.small_Ioc, Nimber.inv_eq_invAux, Nimber.instZeroLEOneClass, Nimber.small_Icc, Nimber.instNoMaxOrder, Nimber.add_eq_zero, Nimber.neg_eq, Nimber.small_Iic, Nimber.one_le_iff_ne_zero, Nimber.lt_wf, Nimber.mul_def, Nimber.small_Ico, Nimber.zero_add, Nimber.add_comm, Ordinal.toNimber_zero, Nimber.add_assoc, Nimber.add_mul, Ordinal.toNimber_toOrdinal, Ordinal.toNimber_max, Ordinal.toNimber_eq_one, Nimber.toOrdinal_symm_eq, SetTheory.PGame.nim_grundyValue, Nimber.mul_comm, SetTheory.PGame.grundyValue_le_of_forall_moveRight, Nimber.toOrdinal_zero, SetTheory.PGame.grundyValue_iff_equiv_zero, Nimber.instIsCancelMulZero, Nimber.le_zero, Nimber.toOrdinal_toNimber, Nimber.small_Iio, Nimber.add_zero, Nimber.mul_one, Nimber.lt_one_iff_zero, SetTheory.PGame.nim_add_nim_equiv, Nimber.toOrdinal_eq_zero, SetTheory.PGame.grundyValue_add
instInhabitedNimber 📖	CompOp	—
instNontrivialNimber 📖	CompOp	—
instOneNimber 📖	CompOp	13 math math: SetTheory.PGame.grundyValue_star, Ordinal.toNimber_one, Nimber.toOrdinal_eq_one, Nimber.cons_mem_invSet, Nimber.mul_invAux_cancel, Nimber.one_mul, Nimber.toOrdinal_one, Nimber.instNeZeroOne, Nimber.instZeroLEOneClass, Nimber.one_le_iff_ne_zero, Ordinal.toNimber_eq_one, Nimber.mul_one, Nimber.lt_one_iff_zero
instWellFoundedRelationNimber 📖	CompOp	—
instZeroNimber 📖	CompOp	19 math math: Ordinal.toNimber_eq_zero, Nimber.instNoZeroDivisors, Nimber.zero_mem_invSet, Nimber.add_self, Nimber.pos_iff_ne_zero, SetTheory.PGame.grundyValue_zero, Nimber.instNeZeroOne, Nimber.not_lt_zero, Nimber.instZeroLEOneClass, Nimber.add_eq_zero, Nimber.zero_add, Ordinal.toNimber_zero, Nimber.toOrdinal_zero, SetTheory.PGame.grundyValue_iff_equiv_zero, Nimber.instIsCancelMulZero, Nimber.le_zero, Nimber.add_zero, Nimber.lt_one_iff_zero, Nimber.toOrdinal_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_small_nimber 📖	mathematical	—	Small Nimber	—	not_small_ordinal

---

← Back to Index