GameAdd

📁 Source: Mathlib/Order/GameAdd.lean

Statistics

Metric	Count
Definitions GameAdd, fix, GameAdd, fix	4
Theorems prod_gameAdd, sym2_gameAdd, fix_eq, induction, to_sym2, gameAdd_iff, gameAdd_le_lex, gameAdd_mk_iff, gameAdd_swap_swap, gameAdd_swap_swap_mk, rprod_le_transGen_gameAdd, fix_eq, fst, fst_snd, induction, snd, snd_fst, gameAdd_iff, gameAdd_mk'_iff, prod_gameAdd, sym2_gameAdd	21
Total	25

Acc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_gameAdd 📖	mathematical	—	Prod.GameAdd	—	—
sym2_gameAdd 📖	mathematical	—	Sym2 Sym2.GameAdd	—	Sym2.ind Sym2.GameAdd.eq_1 Sym2.eq_swap

Prod

Definitions

Name	Category	Theorems
GameAdd 📖	CompData	12 math math: rprod_le_transGen_gameAdd, gameAdd_swap_swap, gameAdd_le_lex, gameAdd_mk_iff, DFinsupp.lex_fibration, Relation.cutExpand_fibration, Sym2.gameAdd_mk'_iff, WellFounded.prod_gameAdd, gameAdd_iff, gameAdd_swap_swap_mk, Acc.prod_gameAdd, Sym2.gameAdd_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gameAdd_iff 📖	mathematical	—	GameAdd	—	—
gameAdd_le_lex 📖	mathematical	—	Pi.hasLe Prop.le GameAdd	—	—
gameAdd_mk_iff 📖	mathematical	—	GameAdd	—	gameAdd_iff
gameAdd_swap_swap 📖	mathematical	—	GameAdd	—	swap.eq_1 gameAdd_mk_iff
gameAdd_swap_swap_mk 📖	mathematical	—	GameAdd	—	gameAdd_swap_swap
rprod_le_transGen_gameAdd 📖	mathematical	—	Pi.hasLe Prop.le GameAdd	—	—

Prod.GameAdd

Definitions

Name	Category	Theorems
fix 📖	CompOp	1 math math: fix_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fix_eq 📖	mathematical	—	fix	—	WellFounded.prod_gameAdd
induction 📖	—	—	—	—	—
to_sym2 📖	mathematical	Prod.GameAdd	Sym2.GameAdd	—	Sym2.gameAdd_iff

Sym2

Definitions

Name	Category	Theorems
GameAdd 📖	MathDef	9 math math: Prod.GameAdd.to_sym2, GameAdd.fst_snd, GameAdd.snd_fst, gameAdd_mk'_iff, GameAdd.fst, WellFounded.sym2_gameAdd, Acc.sym2_gameAdd, GameAdd.snd, gameAdd_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gameAdd_iff 📖	mathematical	—	GameAdd Prod.GameAdd	—	—
gameAdd_mk'_iff 📖	mathematical	—	GameAdd Prod.GameAdd	—	—

Sym2.GameAdd

Definitions

Name	Category	Theorems
fix 📖	CompOp	1 math math: fix_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fix_eq 📖	mathematical	—	fix	—	—
fst 📖	mathematical	—	Sym2.GameAdd	—	Prod.GameAdd.to_sym2
fst_snd 📖	mathematical	—	Sym2.GameAdd	—	Sym2.eq_swap snd
induction 📖	—	—	—	—	—
snd 📖	mathematical	—	Sym2.GameAdd	—	Prod.GameAdd.to_sym2
snd_fst 📖	mathematical	—	Sym2.GameAdd	—	Sym2.eq_swap fst

WellFounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_gameAdd 📖	mathematical	—	Prod.GameAdd	—	Acc.prod_gameAdd
sym2_gameAdd 📖	mathematical	—	Sym2 Sym2.GameAdd	—	Sym2.inductionOn Acc.sym2_gameAdd

---

← Back to Index