| Metric | Count |
|---|
DefinitionsFuzzy, LF, instCoeRelabellingEquiv, instPreorder, instTransEquivLF, instTransEquivLe, instTransEquivLt, instTransLFEquiv, instTransLFLe, instTransLeEquiv, instTransLeLF, instTransLtEquiv, le, leftResponse, rightResponse, setoid, «term_‖_», «term_⧏_» | 18 |
Theoremslf_moveRight, moveLeft_lf, not_gf, trans_lf, lf, trans_lf, ge, isEmpty, le, not_fuzzy, not_fuzzy', of_equiv, of_exists, trans, lf, not_equiv, not_equiv', swap, swap_iff, equiv, ge, le, not_equiv, not_equiv', not_ge, not_gt, trans_le, trans_lt, equiv, ge, le, bddAbove_of_small, bddAbove_range_of_small, bddBelow_of_small, bddBelow_range_of_small, equiv_comm, equiv_congr_left, equiv_congr_right, equiv_def, equiv_of_eq, equiv_refl, equiv_rfl, fuzzy_congr, fuzzy_congr_imp, fuzzy_congr_left, fuzzy_congr_right, fuzzy_irrefl, fuzzy_of_equiv_of_fuzzy, fuzzy_of_fuzzy_of_equiv, insertLeft_equiv_of_lf, insertRight_equiv_of_lf, insertRight_le, instIrreflFuzzy, instIrreflLF, instIsEquivEquiv, instSymmFuzzy, le_congr, le_congr_imp, le_congr_left, le_congr_right, le_def, le_iff_forall_lf, le_insertLeft, le_of_equiv_of_le, le_of_forall_lf, le_of_forall_lt, le_of_le_of_equiv, le_or_gf, le_zero, le_zero_lf, le_zero_of_isEmpty_leftMoves, leftResponse_spec, lf_congr, lf_congr_imp, lf_congr_left, lf_congr_right, lf_def, lf_iff_exists_le, lf_iff_lt_or_fuzzy, lf_irrefl, lf_mk, lf_mk_of_le, lf_moveRight, lf_moveRight_of_le, lf_of_equiv_of_lf, lf_of_fuzzy, lf_of_le_mk, lf_of_le_moveLeft, lf_of_le_of_lf, lf_of_lf_of_equiv, lf_of_lf_of_le, lf_of_lf_of_lt, lf_of_lt, lf_of_lt_of_lf, lf_of_mk_le, lf_of_moveRight_le, lf_or_equiv_or_gf, lf_zero, lf_zero_le, lt_congr, lt_congr_imp, lt_congr_left, lt_congr_right, lt_iff_le_and_lf, lt_of_equiv_of_lt, lt_of_le_of_lf, lt_of_lt_of_equiv, lt_or_equiv_of_le, lt_or_equiv_or_gf, lt_or_equiv_or_gt_or_fuzzy, lt_or_fuzzy_of_lf, mk_le_mk, mk_lf, mk_lf_mk, mk_lf_of_le, moveLeft_lf, moveLeft_lf_of_le, not_fuzzy_of_ge, not_fuzzy_of_le, not_le, not_lf, not_lt, rightResponse_spec, zero_le, zero_le_lf, zero_le_of_isEmpty_rightMoves, zero_lf, zero_lf_le | 128 |
| Total | 146 |
| Name | Category | Theorems |
|---|
Fuzzy 📖 | MathDef | 34 mathmath: Impartial.fuzzy_zero_iff_gf, lt_or_fuzzy_of_lf, fuzzy_iff_game_fuzzy, not_fuzzy_of_ge, star_fuzzy_zero, Fuzzy.swap_iff, lt_or_equiv_or_gt_or_fuzzy, fuzzy_congr, neg_fuzzy_zero_iff, nim_fuzzy_zero_of_ne_zero, Impartial.exists_left_move_equiv_iff_fuzzy_zero, neg_fuzzy_neg_iff, Impartial.not_fuzzy_zero_iff, neg_fuzzy_iff, nim_add_fuzzy_zero_iff, star_fuzzy_down, Impartial.not_equiv_zero_iff, Equiv.not_fuzzy', Impartial.fuzzy_zero_iff_lf, Impartial.equiv_or_fuzzy_zero, fuzzy_congr_left, Equiv.not_fuzzy, instIrreflFuzzy, star_fuzzy_up, fuzzy_congr_right, not_fuzzy_of_le, Impartial.forall_rightMoves_fuzzy_iff_equiv_zero, instSymmFuzzy, not_fuzzy, Impartial.forall_leftMoves_fuzzy_iff_equiv_zero, Impartial.exists_right_move_equiv_iff_fuzzy_zero, fuzzy_irrefl, zero_fuzzy_neg_iff, lf_iff_lt_or_fuzzy
|
LF 📖 | MathDef | 60 mathmath: Ordinal.toPGame_lf_iff, not_lf, star_lf_zero, Impartial.fuzzy_zero_iff_gf, LT.lt.lf, neg_lf_neg_iff, lt_iff_le_and_lf, lf_congr, lf_irrefl, lf_iff_exists_le, lt_or_equiv_or_gf, lf_zero_le, mk_lf_mk, LE.le.not_gf, lf_iff_sub_zero_lf, lf_or_equiv_or_gf, lf_of_mk_le, lf_mk_of_le, Ordinal.toPGame_lf, lf_of_moveRight_le, mk_lf, zero_lf_one, lf_of_le_moveLeft, not_le, mk_le_mk, lf_zero, lf_of_lt, lf_neg_iff, Impartial.lf_zero_iff, lf_def, zero_lf_star, zero_lf_le, le_zero_lf, Impartial.fuzzy_zero_iff_lf, lf_of_fuzzy, zero_lf_inv', lf_congr_right, not_lt, lf_of_le_mk, LE.le.lf_moveRight, neg_lf_zero_iff, lf_congr_left, le_or_gf, moveLeft_lf, lf_moveRight, LE.le.moveLeft_lf, neg_lf_iff, zero_lf, Fuzzy.lf, mk_lf_of_le, instIrreflLF, zero_le_lf, lf_moveRight_of_le, moveLeft_lf_of_le, lf_iff_lt, lf_mk, zero_lf_neg_iff, lf_iff_game_lf, le_iff_forall_lf, lf_iff_lt_or_fuzzy
|
instCoeRelabellingEquiv 📖 | CompOp | — |
instPreorder 📖 | CompOp | 45 mathmath: lt_or_equiv_or_gt, powHalf_succ_lt_one, lt_congr, lt_iff_le_and_lf, lt_congr_right, lt_or_fuzzy_of_lf, lt_iff_exists_le, powHalf_succ_lt_powHalf, neg_lt_zero_iff, neg_lt_neg_iff, lt_or_equiv_or_gf, lt_iff_game_lt, Impartial.nonneg, le_iff_forall_lt, addRightStrictMono, lt_neg_iff, lt_iff_sub_pos, lt_or_equiv_or_gt_or_fuzzy, Numeric.left_lt_right, Surreal.zero_lt_mk, zero_lt_one, LF.lt, neg_lt_iff, Impartial.nonpos, up_neg, lt_def, zero_lt_neg_iff, lt_congr_left, not_lt, powHalf_pos, Ordinal.toPGame_lt_iff, lt_of_exists_le, Numeric.lt_moveRight, down_neg, LF.not_gt, numeric_def, lt_or_equiv_of_le, lt_of_le_of_lf, Numeric.moveLeft_lt, lt_of_lf, addLeftStrictMono, Surreal.mk_lt_mk, lf_iff_lt, Ordinal.toPGame_lt, lf_iff_lt_or_fuzzy
|
instTransEquivLF 📖 | CompOp | — |
instTransEquivLe 📖 | CompOp | — |
instTransEquivLt 📖 | CompOp | — |
instTransLFEquiv 📖 | CompOp | — |
instTransLFLe 📖 | CompOp | — |
instTransLeEquiv 📖 | CompOp | — |
instTransLeLF 📖 | CompOp | — |
instTransLtEquiv 📖 | CompOp | — |
le 📖 | CompOp | 74 mathmath: not_lf, zero_le_of_isEmpty_rightMoves, le_congr_right, Impartial.le_zero_iff, neg_le_neg_iff, lt_iff_le_and_lf, addLeftMono, lt_iff_exists_le, Impartial.equiv_zero_iff_le, le_birthday, lf_iff_exists_le, le_of_forall_lf, lf_zero_le, powHalf_le_one, addRightMono, le_iff_forall_lt, le_def, mk_lf_mk, equiv_def, LF.not_ge, Relabelling.le, add_comm_le, Impartial.equiv_zero_iff_ge, not_le, Identical.ge, Identical.le, le_zero, mk_le_mk, le_of_forall_lt, zero_le, le_neg_iff, le_zero_of_isEmpty_leftMoves, bddAbove_of_small, Ordinal.toPGame_nonneg, bddBelow_of_small, Surreal.Multiplication.mul_right_le_of_equiv, powHalf_succ_le_powHalf, zero_lf_le, le_zero_lf, le_congr_left, Ordinal.toPGame_le, instZeroLEOneClass, not_lt, zero_le_add_neg_cancel, zero_le_neg_add_cancel, le_iff_game_le, zero_le_powHalf, bddBelow_range_of_small, neg_add_le, le_or_gf, le_congr, LF.le, le_iff_sub_nonneg, Surreal.zero_le_mk, zero_le_neg_iff, Equiv.ge, bddAbove_range_of_small, neg_le_iff, Numeric.moveLeft_le, insertRight_le, Relabelling.ge, neg_le_zero_iff, Ordinal.toPGame_le_iff, zero_le_lf, add_neg_cancel_le_zero, neg_add_cancel_le_zero, Ordinal.toPGameEmbedding_apply, le_insertLeft, Numeric.le_moveRight, neg_birthday_le, Surreal.mk_le_mk, le_iff_forall_lf, Equiv.le, le_of_lf
|
leftResponse 📖 | CompOp | 1 mathmath: leftResponse_spec
|
rightResponse 📖 | CompOp | 1 mathmath: rightResponse_spec
|
setoid 📖 | CompOp | 115 mathmath: nim_add_equiv_zero_iff, lt_or_equiv_or_gt, quot_neg_mul, sub_self_equiv, Impartial.mk'_add_self, right_distrib_equiv, quot_one, grundyValue_eq_iff_equiv_nim, one_mul_equiv, Impartial.equiv_zero_iff_le, Surreal.Multiplication.mulOption_lt_mul_iff_P3, equiv_iff_game_eq, quot_right_distrib_sub, fuzzy_iff_game_fuzzy, Impartial.add_self, grundyValue_eq_iff_equiv, Ordinal.toPGame_zero, quot_natCast, quot_mul_neg, lt_or_equiv_or_gf, Ordinal.toPGame_nmul, lt_iff_game_lt, inv_one_equiv, rightMoves_mul_iff, SetTheory.Game.zero_def, quot_mul_one, nim_one_equiv, Surreal.mk_eq_mk, quot_left_distrib_sub, equiv_comm, equiv_refl, SetTheory.Game.birthday_eq_pGameBirthday, mul_one_equiv, equiv_def, LF.not_equiv', Fuzzy.not_equiv, Ordinal.toPGame_one, lf_or_equiv_or_gf, neg_equiv_iff, Fuzzy.not_equiv', Equiv.isEmpty, lt_or_equiv_or_gt_or_fuzzy, mul_zero_equiv, Impartial.exists_left_move_equiv_iff_fuzzy_zero, quot_left_distrib, Impartial.equiv_zero_iff_ge, zero_add_equiv, left_distrib_equiv, Surreal.Multiplication.mulOption_lt, equiv_congr_right, mulOption_symm, mul_assoc_equiv, quot_one_mul, equiv_congr_left, neg_equiv_zero_iff, inv'_one_equiv, add_comm_equiv, Impartial.mk'_neg_equiv_self, Impartial.equiv_iff_add_equiv_zero, Impartial.not_fuzzy_zero_iff, equiv_nim_grundyValue, leftMoves_mul_iff, insertLeft_equiv_of_lf, Ordinal.mk_toPGame, add_assoc_equiv, Impartial.not_equiv_zero_iff, neg_add_cancel_equiv, neg_equiv_neg_iff, Impartial.equiv_or_fuzzy_zero, mul_comm_equiv, add_zero_equiv, impartial_def, nim_zero_equiv, Ordinal.toPGame_natCast, quot_mul_comm, Surreal.Multiplication.mulOption_lt_iff_P1, equiv_rfl, add_neg_cancel_equiv, Ordinal.toGame_nmul, quot_mul_zero, LF.not_equiv, zero_mul_equiv, le_iff_game_le, add_powHalf_succ_self_eq_powHalf, Identical.equiv, nim_equiv_iff_eq, Impartial.forall_rightMoves_fuzzy_iff_equiv_zero, equiv_of_eq, Surreal.Multiplication.mulOption_lt_of_lt, SetTheory.Game.birthday_star, quot_mul_assoc, Relabelling.equiv, quot_neg, quot_right_distrib, Surreal.mk_eq_zero, insertRight_equiv_of_lf, quot_zero_mul, Ordinal.toPGame_nadd, Impartial.equiv_iff_add_equiv_zero', Impartial.forall_leftMoves_fuzzy_iff_equiv_zero, half_add_half_equiv_one, SetTheory.Game.birthday_quot_le_pGameBirthday, Impartial.exists_right_move_equiv_iff_fuzzy_zero, lt_or_equiv_of_le, inv'_zero_equiv, grundyValue_iff_equiv_zero, quot_neg_mul_neg, Impartial.neg_equiv_self, quot_zero, quot_add, quot_sub, nim_add_nim_equiv, zero_equiv_neg_iff, lf_iff_game_lf, Ordinal.toPGame_equiv_iff
|
«term_‖_» 📖 | CompOp | — |
«term_⧏_» 📖 | CompOp | — |