def MisereSetoid {G : Type (u + 1)} [Form G] (A : G → Prop) : Setoid { g : G // A g }

Restricted misère equality modulo A, as a setoid on A's games.

Equations

• MisereSetoid A = { r := fun (g h : { g : G // A g }) => ↑g =m A↑h, iseqv := ⋯ }

def MisereQuotient {G : Type (u + 1)} [Form G] (A : G → Prop) : Type (u + 1)

The games in A taken up to misère equality modulo A.

Equations

• MisereQuotient A = Quotient (MisereSetoid A)

@[instance_reducible]

instance instSetoidSubtype_combinatorialGames {G : Type (u + 1)} [Form G] (A : G → Prop) : Setoid { g : G // A g }

Equations

• instSetoidSubtype_combinatorialGames A = MisereSetoid A

def Form.MisereQuotient.mk {G : Type (u + 1)} [Form G] {A : G → Prop} (g : { g : G // A g }) : MisereQuotient A

The class of a game in the misère quotient.

Equations

• Form.MisereQuotient.mk g = ⟦g⟧

def Form.MisereQuotient.out {G : Type (u + 1)} [Form G] {A : G → Prop} (x : MisereQuotient A) : { g : G // A g }

A chosen representative of a misère-quotient class.

Equations

• Form.MisereQuotient.out x = Quotient.out x

theorem Form.MisereQuotient.mk_eq_mk {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : { g : G // A g }} : mk g = mk h ↔ ↑g =m A↑h

theorem Form.MisereQuotient.sound {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : { g : G // A g }} (hgh : ↑g =m A↑h) : mk g = mk h

theorem Form.MisereQuotient.exact {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : { g : G // A g }} (hgh : mk g = mk h) : ↑g =m A↑h

@[simp]

theorem Form.MisereQuotient.mk_out {G : Type (u + 1)} [Form G] {A : G → Prop} (x : MisereQuotient A) : mk (out x) = x

theorem Form.MisereQuotient.out_equiv_self {G : Type (u + 1)} [Form G] {A : G → Prop} (g : { g : G // A g }) : ↑(out (mk g)) =m A↑g

theorem Form.MisereQuotient.add_misereEQ_add {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAdd A] {g g' h h' : G} (hh : A h) (hg' : A g') (hg : g =m A g') (hh' : h =m A h') : (g + h) =m A g' + h'

theorem Form.MisereQuotient.add_misereGE_add_right {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAdd A] {k : G} (hk : A k) {g h : G} (hgh : g ≥m A h) : (g + k) ≥m A h + k

@[instance_reducible]

instance Form.MisereQuotient.instAdd {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAdd A] : Add (MisereQuotient A)

Equations

• Form.MisereQuotient.instAdd = { add := fun (x y : MisereQuotient A) => Quotient.liftOn₂ x y (fun (g h : { g : G // A g }) => Form.MisereQuotient.mk ⟨↑g + ↑h, ⋯⟩) ⋯ }

@[simp]

theorem Form.MisereQuotient.mk_add_mk {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAdd A] (g h : { g : G // A g }) : mk g + mk h = mk ⟨↑g + ↑h, ⋯⟩

@[instance_reducible]

instance Form.MisereQuotient.instAddCommSemigroup {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAdd A] : AddCommSemigroup (MisereQuotient A)

Equations

• Form.MisereQuotient.instAddCommSemigroup = { toAdd := Form.MisereQuotient.instAdd, add_assoc := ⋯, add_comm := ⋯ }

@[instance_reducible]

instance Form.MisereQuotient.instZero {G : Type (u + 1)} [Form G] {A : G → Prop} [HasZero A] : Zero (MisereQuotient A)

Equations

• Form.MisereQuotient.instZero = { zero := Form.MisereQuotient.mk ⟨0, ⋯⟩ }

@[simp]

theorem Form.MisereQuotient.mk_zero {G : Type (u + 1)} [Form G] {A : G → Prop} [HasZero A] : mk ⟨0, ⋯⟩ = 0

@[instance_reducible]

instance Form.MisereQuotient.instAddCommMonoid {G : Type (u + 1)} [Form G] {A : G → Prop} [HasZero A] [ClosedUnderAdd A] : AddCommMonoid (MisereQuotient A)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Form.MisereQuotient.instLE {G : Type (u + 1)} [Form G] {A : G → Prop} : LE (MisereQuotient A)

The order on the quotient: mk g ≤ mk h exactly when h ≥m A g.

Equations

• Form.MisereQuotient.instLE = { le := fun (x y : MisereQuotient A) => Quotient.liftOn₂ x y (fun (g h : { g : G // A g }) => ↑h ≥m A↑g) ⋯ }

theorem Form.MisereQuotient.mk_le_mk {G : Type (u + 1)} [Form G] {A : G → Prop} (g h : { g : G // A g }) : mk g ≤ mk h ↔ ↑h ≥m A↑g

@[instance_reducible]

instance Form.MisereQuotient.instPartialOrder {G : Type (u + 1)} [Form G] {A : G → Prop} : PartialOrder (MisereQuotient A)

Equations

• Form.MisereQuotient.instPartialOrder = { le := fun (x1 x2 : MisereQuotient A) => x1 ≤ x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Form.MisereQuotient.out_le_out {G : Type (u + 1)} [Form G] {A : G → Prop} {a b : MisereQuotient A} : a ≤ b ↔ ↑(out b) ≥m A↑(out a)

instance Form.MisereQuotient.instIsOrderedAddMonoid {G : Type (u + 1)} [Form G] {A : G → Prop} [HasZero A] [ClosedUnderAdd A] : IsOrderedAddMonoid (MisereQuotient A)