Theorems · Definition · order theory
Sym2.GameAdd
{α : Type u_1} → (α → α → Prop) → Sym2 α → Sym2 α → PropSym2.GameAdd rα x y means that x can be reached from y by decreasing either entry with
respect to the relation rα.
See Prod.GameAdd for the ordered pair analog.
- Defined in
- Mathlib.Order.GameAdd
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Sym2statement · cited by 737
- Prod.GameAddproof · cited by 18
- Sym2.lift₂proof · cited by 3
Cited by16
Results whose statement or proof uses this declaration.
- Sym2.GameAdd.recursionstatement and proof · cited by 5
- ZFSet.IsOrdinal.notMem_iff_subsetproof · cited by 3
- Sym2.GameAdd.fst_sndstatement and proof · cited by 2
- ZFSet.IsOrdinal.subset_iff_eq_or_memproof · cited by 2
- Prod.GameAdd.to_sym2statement · cited by 2
- Sym2.GameAdd.fststatement · cited by 1
- Sym2.GameAdd.recursion_eqstatement and proof · cited by 1
- Sym2.GameAdd.sndstatement · cited by 1
- Sym2.gameAdd_iffstatement · cited by 1
- Acc.sym2_gameAddstatement and proof · cited by 1
- Sym2.GameAdd.fix_eqstatement · cited by 0
- Sym2.GameAdd.inductionstatement and proof · cited by 0