Basic

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

Statistics

Metric	Count
Definitions `toSurreal`, `Numeric`, `Surreal`, `addCommGroup`, `instAdd`, `instAddMonoidWithOne`, `instInhabited`, `instLE`, `instLT`, `instLinearOrder`, `instNeg`, `instOne`, `instZero`, `lift₂`, `mk`, `partialOrder`, `toGame`	17
Theorems `le`, `lt`, `add`, `isOption`, `le_moveRight`, `left_lt_right`, `lt_moveRight`, `mk`, `moveLeft`, `moveLeft_le`, `moveLeft_lt`, `moveRight`, `neg`, `sub`, `numeric_congr`, `numeric_imp`, `insertLeft_numeric`, `insertRight_numeric`, `le_iff_forall_lt`, `le_of_lf`, `lf_asymm`, `lf_iff_lt`, `lt_def`, `lt_iff_exists_le`, `lt_of_exists_le`, `lt_of_lf`, `lt_or_equiv_or_gt`, `not_fuzzy`, `numeric_def`, `numeric_nat`, `numeric_of_isEmpty`, `numeric_of_isEmpty_leftMoves`, `numeric_of_isEmpty_rightMoves`, `numeric_one`, `numeric_rec`, `numeric_toPGame`, `numeric_zero`, `bddAbove_of_small`, `bddAbove_range_of_small`, `bddBelow_of_small`, `bddBelow_range_of_small`, `isOrderedAddMonoid`, `mk_add`, `mk_eq_mk`, `mk_eq_zero`, `mk_le_mk`, `mk_lt_mk`, `mk_lt_mk_moveRight`, `mk_moveLeft_lt_mk`, `mk_sub`, `nat_toGame`, `one_toGame`, `zero_def`, `zero_le_mk`, `zero_lt_mk`, `zero_toGame`	56
Total	73

Ordinal

Definitions

Name	Category	Theorems
`toSurreal` 📖	CompOp	—

SetTheory.PGame

Definitions

Name	Category	Theorems
`Numeric` 📖	MathDef	14 math math: `Surreal.Multiplication.Args.numeric_P24`, `Surreal.Multiplication.numeric_mul_option`, `Surreal.Multiplication.numeric_of_ih`, `numeric_toPGame`, `Surreal.Multiplication.numeric_option_mul_option`, `Surreal.Multiplication.numeric_option_mul`, `numeric_powHalf`, `Relabelling.numeric_congr`, `numeric_one`, `numeric_zero`, `numeric_def`, `Surreal.Multiplication.Args.numeric_P1`, `numeric_of_isEmpty`, `numeric_nat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`insertLeft_numeric` 📖	mathematical	`Numeric` `SetTheory.PGame` `le`	`insertLeft`	—	`Numeric.eq_def` `le_iff_forall_lt`
`insertRight_numeric` 📖	mathematical	`Numeric` `SetTheory.PGame` `le`	`insertRight`	—	`neg_neg` `neg_insertLeft_neg` `Numeric.neg` `insertLeft_numeric` `neg_le_neg_iff`
`le_iff_forall_lt` 📖	mathematical	`Numeric`	`SetTheory.PGame` `le` `Preorder.toLT` `instPreorder` `moveLeft` `moveRight`	—	`le_iff_forall_lf` `lf_iff_lt` `Numeric.moveLeft` `Numeric.moveRight`
`le_of_lf` 📖	mathematical	`LF` `Numeric`	`SetTheory.PGame` `le`	—	`not_lf` `lf_asymm`
`lf_asymm` 📖	—	`Numeric` `LF`	—	—	`LE.le.moveLeft_lf` `LE.le.not_gf` `le_trans` `lf_of_lt` `LE.le.lf_moveRight`
`lf_iff_lt` 📖	mathematical	`Numeric`	`LF` `SetTheory.PGame` `Preorder.toLT` `instPreorder`	—	`LF.lt` `lf_of_lt`
`lt_def` 📖	mathematical	`Numeric`	`SetTheory.PGame` `Preorder.toLT` `instPreorder` `moveLeft` `moveRight`	—	`lf_iff_lt` `lf_def` `Numeric.moveLeft` `Numeric.moveRight`
`lt_iff_exists_le` 📖	mathematical	`Numeric`	`SetTheory.PGame` `Preorder.toLT` `instPreorder` `le` `moveLeft` `moveRight`	—	`lf_iff_lt` `lf_iff_exists_le`
`lt_of_exists_le` 📖	mathematical	`Numeric` `SetTheory.PGame` `le` `moveLeft` `moveRight`	`Preorder.toLT` `instPreorder`	—	`lt_iff_exists_le`
`lt_of_lf` 📖	mathematical	`LF` `Numeric`	`SetTheory.PGame` `Preorder.toLT` `instPreorder`	—	`lt_or_fuzzy_of_lf` `not_fuzzy_of_le` `LF.le`
`lt_or_equiv_or_gt` 📖	mathematical	`Numeric`	`SetTheory.PGame` `Preorder.toLT` `instPreorder` `setoid`	—	`LF.lt` `lf_or_equiv_or_gf`
`not_fuzzy` 📖	mathematical	`Numeric`	`Fuzzy`	—	`not_lf` `LF.le` `lf_of_fuzzy`
`numeric_def` 📖	mathematical	—	`Numeric` `SetTheory.PGame` `Preorder.toLT` `instPreorder` `moveLeft` `moveRight`	—	—
`numeric_nat` 📖	mathematical	—	`Numeric` `SetTheory.PGame` `instNatCast`	—	`numeric_zero` `Numeric.add` `numeric_one`
`numeric_of_isEmpty` 📖	mathematical	—	`Numeric`	—	—
`numeric_of_isEmpty_leftMoves` 📖	—	`Numeric` `moveRight`	—	—	—
`numeric_of_isEmpty_rightMoves` 📖	—	`Numeric` `moveLeft`	—	—	—
`numeric_one` 📖	mathematical	—	`Numeric` `SetTheory.PGame` `instOnePGame`	—	`numeric_of_isEmpty_rightMoves` `isEmpty_one_rightMoves` `numeric_zero`
`numeric_rec` 📖	—	`Numeric`	—	—	—
`numeric_toPGame` 📖	mathematical	—	`Numeric` `Ordinal.toPGame`	—	`Ordinal.induction` `numeric_of_isEmpty_rightMoves` `Ordinal.isEmpty_toPGame_rightMoves` `Ordinal.toPGame_moveLeft'` `Ordinal.toLeftMovesToPGame_symm_lt`
`numeric_zero` 📖	mathematical	—	`Numeric` `SetTheory.PGame` `instZero`	—	`numeric_of_isEmpty` `isEmpty_zero_leftMoves` `isEmpty_zero_rightMoves`

SetTheory.PGame.LF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le` 📖	mathematical	`SetTheory.PGame.LF` `SetTheory.PGame.Numeric`	`SetTheory.PGame` `SetTheory.PGame.le`	—	`SetTheory.PGame.le_of_lf`
`lt` 📖	mathematical	`SetTheory.PGame.LF` `SetTheory.PGame.Numeric`	`SetTheory.PGame` `Preorder.toLT` `SetTheory.PGame.instPreorder`	—	`SetTheory.PGame.lt_of_lf`

SetTheory.PGame.Numeric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `SetTheory.PGame.instAdd`	—	—
`isOption` 📖	—	`SetTheory.PGame.IsOption` `SetTheory.PGame.Numeric`	—	—	`moveLeft` `moveRight`
`le_moveRight` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `SetTheory.PGame.le` `SetTheory.PGame.moveRight`	—	`LT.lt.le` `lt_moveRight`
`left_lt_right` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `Preorder.toLT` `SetTheory.PGame.instPreorder` `SetTheory.PGame.moveLeft` `SetTheory.PGame.moveRight`	—	—
`lt_moveRight` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `Preorder.toLT` `SetTheory.PGame.instPreorder` `SetTheory.PGame.moveRight`	—	`SetTheory.PGame.LF.lt` `SetTheory.PGame.lf_moveRight` `moveRight`
`mk` 📖	—	`SetTheory.PGame` `Preorder.toLT` `SetTheory.PGame.instPreorder` `SetTheory.PGame.moveLeft` `SetTheory.PGame.moveRight` `SetTheory.PGame.Numeric`	—	—	`SetTheory.PGame.numeric_def`
`moveLeft` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame.moveLeft`	—	—
`moveLeft_le` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `SetTheory.PGame.le` `SetTheory.PGame.moveLeft`	—	`LT.lt.le` `moveLeft_lt`
`moveLeft_lt` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `Preorder.toLT` `SetTheory.PGame.instPreorder` `SetTheory.PGame.moveLeft`	—	`SetTheory.PGame.LF.lt` `SetTheory.PGame.moveLeft_lf` `moveLeft`
`moveRight` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame.moveRight`	—	—
`neg` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `SetTheory.PGame.instNeg`	—	`SetTheory.PGame.neg_lt_neg_iff`
`sub` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `SetTheory.PGame.instSub`	—	`add` `neg`

SetTheory.PGame.Relabelling

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`numeric_congr` 📖	mathematical	—	`SetTheory.PGame.Numeric`	—	`numeric_imp`
`numeric_imp` 📖	—	`SetTheory.PGame.Numeric`	—	—	`SetTheory.PGame.lt_congr` `equiv` `SetTheory.PGame.Numeric.left_lt_right` `SetTheory.PGame.Numeric.moveLeft` `SetTheory.PGame.Numeric.moveRight`

Surreal

Definitions

Name	Category	Theorems
`addCommGroup` 📖	CompOp	2 math math: `isOrderedAddMonoid`, `mk_sub`
`instAdd` 📖	CompOp	1 math math: `mk_add`
`instAddMonoidWithOne` 📖	CompOp	9 math math: `nsmul_pow_two_powHalf`, `zsmul_pow_two_powHalf`, `nat_toGame`, `dyadicMap_apply`, `zero_toGame`, `double_powHalf_succ_eq_powHalf`, `dyadicMap_apply_pow`, `nsmul_pow_two_powHalf'`, `one_toGame`
`instInhabited` 📖	CompOp	—
`instLE` 📖	CompOp	7 math math: `instZeroLEOneClass`, `bddBelow_range_of_small`, `bddAbove_range_of_small`, `bddBelow_of_small`, `zero_le_mk`, `bddAbove_of_small`, `mk_le_mk`
`instLT` 📖	CompOp	4 math math: `mk_lt_mk_moveRight`, `zero_lt_mk`, `mk_moveLeft_lt_mk`, `mk_lt_mk`
`instLinearOrder` 📖	CompOp	—
`instNeg` 📖	CompOp	—
`instOne` 📖	CompOp	4 math math: `instZeroLEOneClass`, `nsmul_pow_two_powHalf`, `powHalf_zero`, `one_toGame`
`instZero` 📖	CompOp	6 math math: `instZeroLEOneClass`, `zero_def`, `zero_lt_mk`, `zero_toGame`, `zero_le_mk`, `mk_eq_zero`
`lift₂` 📖	CompOp	—
`mk` 📖	CompOp	—
`partialOrder` 📖	CompOp	5 math math: `instIsStrictOrderedRing`, `nat_toGame`, `zero_toGame`, `isOrderedAddMonoid`, `one_toGame`
`toGame` 📖	CompOp	3 math math: `nat_toGame`, `zero_toGame`, `one_toGame`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_of_small` 📖	mathematical	—	`BddAbove` `Surreal` `instLE`	—	`Subtype.range_coe_subtype` `bddAbove_range_of_small`
`bddAbove_range_of_small` 📖	mathematical	—	`BddAbove` `Surreal` `instLE` `Set.range`	—	`Quotient.induction_on_pi` `Subtype.prop` `PEmpty.instIsEmpty` `SetTheory.PGame.Numeric.moveLeft` `Set.forall_mem_range` `Equiv.symm_apply_apply` `SetTheory.PGame.le_iff_forall_lf` `SetTheory.PGame.moveLeft_lf`
`bddBelow_of_small` 📖	mathematical	—	`BddBelow` `Surreal` `instLE`	—	`Subtype.range_coe_subtype` `bddBelow_range_of_small`
`bddBelow_range_of_small` 📖	mathematical	—	`BddBelow` `Surreal` `instLE` `Set.range`	—	`Quotient.induction_on_pi` `Subtype.prop` `PEmpty.instIsEmpty` `SetTheory.PGame.Numeric.moveRight` `Set.forall_mem_range` `Equiv.symm_apply_apply` `SetTheory.PGame.le_iff_forall_lf` `SetTheory.PGame.lf_moveRight`
`isOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `Surreal` `AddCommGroup.toAddCommMonoid` `addCommGroup` `partialOrder`	—	`add_le_add_left` `SetTheory.PGame.addRightMono`
`mk_add` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `SetTheory.PGame.instAdd` `SetTheory.PGame.Numeric.add` `Surreal` `instAdd`	—	`SetTheory.PGame.Numeric.add`
`mk_eq_mk` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `SetTheory.PGame.setoid`	—	`Quotient.eq`
`mk_eq_zero` 📖	mathematical	`SetTheory.PGame.Numeric`	`Surreal` `instZero` `SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instZero`	—	`Quotient.eq` `SetTheory.PGame.numeric_zero`
`mk_le_mk` 📖	mathematical	`SetTheory.PGame.Numeric`	`Surreal` `instLE` `SetTheory.PGame` `SetTheory.PGame.le`	—	—
`mk_lt_mk` 📖	mathematical	`SetTheory.PGame.Numeric`	`Surreal` `instLT` `SetTheory.PGame` `Preorder.toLT` `SetTheory.PGame.instPreorder`	—	—
`mk_lt_mk_moveRight` 📖	mathematical	`SetTheory.PGame.Numeric`	`Surreal` `instLT` `SetTheory.PGame.moveRight` `SetTheory.PGame.Numeric.moveRight`	—	`SetTheory.PGame.Numeric.lt_moveRight`
`mk_moveLeft_lt_mk` 📖	mathematical	`SetTheory.PGame.Numeric`	`Surreal` `instLT` `SetTheory.PGame.moveLeft` `SetTheory.PGame.Numeric.moveLeft`	—	`SetTheory.PGame.Numeric.moveLeft_lt`
`mk_sub` 📖	mathematical	`SetTheory.PGame.Numeric`	`SetTheory.PGame` `SetTheory.PGame.instSub` `SetTheory.PGame.Numeric.sub` `Surreal` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`SetTheory.PGame.Numeric.sub`
`nat_toGame` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Surreal` `SetTheory.Game` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instAddMonoidWithOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `SetTheory.Game.instAddCommGroupWithOneGame` `OrderAddMonoidHom.instFunLike` `toGame` `AddMonoidWithOne.toNatCast`	—	`map_natCast'` `OrderAddMonoidHom.instAddMonoidHomClass` `one_toGame`
`one_toGame` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Surreal` `SetTheory.Game` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instAddMonoidWithOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `SetTheory.Game.instAddCommGroupWithOneGame` `OrderAddMonoidHom.instFunLike` `toGame` `instOne` `AddMonoidWithOne.toOne`	—	—
`zero_def` 📖	mathematical	—	`Surreal` `instZero` `SetTheory.PGame` `SetTheory.PGame.instZero` `SetTheory.PGame.numeric_zero`	—	—
`zero_le_mk` 📖	mathematical	`SetTheory.PGame.Numeric`	`Surreal` `instLE` `instZero` `SetTheory.PGame` `SetTheory.PGame.le` `SetTheory.PGame.instZero`	—	—
`zero_lt_mk` 📖	mathematical	`SetTheory.PGame.Numeric`	`Surreal` `instLT` `instZero` `SetTheory.PGame` `Preorder.toLT` `SetTheory.PGame.instPreorder` `SetTheory.PGame.instZero`	—	—
`zero_toGame` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Surreal` `SetTheory.Game` `PartialOrder.toPreorder` `partialOrder` `SetTheory.Game.instPartialOrderGame` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instAddMonoidWithOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `SetTheory.Game.instAddCommGroupWithOneGame` `OrderAddMonoidHom.instFunLike` `toGame` `instZero` `SetTheory.Game.instZero`	—	—

(root)

Definitions

Name	Category	Theorems
`Surreal` 📖	CompOp	30 math math: `Surreal.mk_lt_mk_moveRight`, `Surreal.instZeroLEOneClass`, `Surreal.nsmul_pow_two_powHalf`, `Surreal.zero_def`, `Surreal.zsmul_pow_two_powHalf`, `Surreal.dyadicMap_apply_pow'`, `Surreal.instIsStrictOrderedRing`, `Surreal.powHalf_zero`, `Surreal.zero_lt_mk`, `Surreal.bddBelow_range_of_small`, `Surreal.mk_moveLeft_lt_mk`, `Surreal.bddAbove_range_of_small`, `Surreal.nat_toGame`, `Surreal.bddBelow_of_small`, `Surreal.dyadicMap_apply`, `Surreal.zero_toGame`, `Surreal.zero_le_mk`, `Surreal.mk_eq_zero`, `Surreal.isOrderedAddMonoid`, `Surreal.mk_sub`, `Surreal.bddAbove_of_small`, `Surreal.instNontrivial`, `Surreal.dyadic_aux`, `Surreal.double_powHalf_succ_eq_powHalf`, `Surreal.mk_lt_mk`, `Surreal.mk_add`, `Surreal.dyadicMap_apply_pow`, `Surreal.nsmul_pow_two_powHalf'`, `Surreal.one_toGame`, `Surreal.mk_le_mk`

---

← Back to Index