Misere combinatorial games.

class MisereGames.ClosedUnderDicotic {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : Prop

Closure under nonempty dicotic set construction inside an ambient predicate.

• closed_dicotic (B C : Set G) [Small.{u, u + 1} ↑B] [Small.{u, u + 1} ↑C] (hB : ∀ b ∈ B, A b) (hC : ∀ c ∈ C, A c) : B.Nonempty → C.Nonempty → IsAmbient !{B | C} → A !{B | C}

@[reducible, inline]

abbrev MisereGames.ClosedUnderLongDicotic {G : Type (u + 1)} [Form G] (A : G → Prop) : Prop

Closure under nonempty dicotic construction in the long ambient space.

Equations

• MisereGames.ClosedUnderLongDicotic A = MisereGames.ClosedUnderDicotic MisereGames.Form.IsLong A

@[reducible, inline]

abbrev MisereGames.ClosedUnderShortDicotic {G : Type (u + 1)} [Form G] (A : G → Prop) : Prop

Closure under nonempty dicotic construction in the short ambient space.

Equations

• MisereGames.ClosedUnderShortDicotic A = MisereGames.ClosedUnderDicotic MisereGames.Form.IsShort A

instance MisereGames.instClosedUnderAddIsShort {G : Type (u + 1)} [Form G] : Form.ClosedUnderAdd Form.IsShort

instance MisereGames.instHereditaryIsShort {G : Type (u + 1)} [Form G] : Form.Hereditary Form.IsShort

instance MisereGames.instClosedUnderDicoticIsShort {G : Type (u + 1)} [Form G] : ClosedUnderDicotic Form.IsShort Form.IsShort

theorem MisereGames.Form.ClosedUnderAdd.sInf_closed {G : Type (u + 1)} [Form G] {S : Set (G → Prop)} (hS : ∀ A ∈ S, ClosedUnderAdd A) : ClosedUnderAdd (sInf S)

@[reducible, inline]

noncomputable abbrev MisereGames.Form.ClosedUnderAdd.closureOperator {G : Type (u + 1)} [Form G] : ClosureOperator (G → Prop)

The closure operator for finding the smallest additively closed set containing the given set.

Equations

• MisereGames.Form.ClosedUnderAdd.closureOperator = ClosureOperator.ofCompletePred (fun (A : G → Prop) => MisereGames.Form.ClosedUnderAdd A) ⋯

@[reducible, inline]

noncomputable abbrev MisereGames.Form.ClosedUnderAdd.closure {G : Type (u + 1)} [Form G] (A : G → Prop) : G → Prop

The additive closure of a given set.

Equations

• MisereGames.Form.ClosedUnderAdd.closure A = MisereGames.Form.ClosedUnderAdd.closureOperator A

theorem MisereGames.Form.ClosedUnderAdd.subset_closure {G : Type (u + 1)} [Form G] (A : G → Prop) : A ≤ closure A

theorem MisereGames.Form.ClosedUnderAdd.mem_closure_of_mem {G : Type (u + 1)} [Form G] {A : G → Prop} {g : G} (hg : A g) : closure A g

instance MisereGames.Form.ClosedUnderAdd.closure_closed {G : Type (u + 1)} [Form G] (A : G → Prop) : ClosedUnderAdd (closure A)

theorem MisereGames.Form.ClosedUnderAdd.add_mem_closure {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : G} (hg : closure A g) (hh : closure A h) : closure A (g + h)

theorem MisereGames.Form.ClosedUnderAdd.closure_min {G : Type (u + 1)} [Form G] {A B : G → Prop} (hAB : A ≤ B) [ClosedUnderAdd B] : closure A ≤ B

theorem MisereGames.Form.ClosedUnderAdd.closure_le {G : Type (u + 1)} [Form G] {A B : G → Prop} [ClosedUnderAdd B] : closure A ≤ B ↔ A ≤ B

theorem MisereGames.Form.ClosedUnderAdd.closure_mono {G : Type (u + 1)} [Form G] {A B : G → Prop} (hAB : A ≤ B) : closure A ≤ closure B

theorem MisereGames.Form.Hereditary.sInf_closed {G : Type (u + 1)} [Form G] {S : Set (G → Prop)} (hS : ∀ A ∈ S, Hereditary A) : Hereditary (sInf S)

@[reducible, inline]

noncomputable abbrev MisereGames.Form.Hereditary.closureOperator {G : Type (u + 1)} [Form G] : ClosureOperator (G → Prop)

The closure operator for finding the smallest hereditary set containing the given set.

Equations

• MisereGames.Form.Hereditary.closureOperator = ClosureOperator.ofCompletePred (fun (A : G → Prop) => MisereGames.Form.Hereditary A) ⋯

@[reducible, inline]

noncomputable abbrev MisereGames.Form.Hereditary.closure {G : Type (u + 1)} [Form G] (A : G → Prop) : G → Prop

The hereditary closure of a given set.

Equations

• MisereGames.Form.Hereditary.closure A = MisereGames.Form.Hereditary.closureOperator A

theorem MisereGames.Form.Hereditary.subset_closure {G : Type (u + 1)} [Form G] (A : G → Prop) : A ≤ closure A

theorem MisereGames.Form.Hereditary.mem_closure_of_mem {G : Type (u + 1)} [Form G] {A : G → Prop} {g : G} (hg : A g) : closure A g

instance MisereGames.Form.Hereditary.closure_closed {G : Type (u + 1)} [Form G] (A : G → Prop) : Hereditary (closure A)

theorem MisereGames.Form.Hereditary.has_option_mem_closure {G : Type (u + 1)} [Form G] {A : G → Prop} {g g' : G} (hg : closure A g) (h : IsOption g' g) : closure A g'

theorem MisereGames.Form.Hereditary.closure_min {G : Type (u + 1)} [Form G] {A B : G → Prop} (hAB : A ≤ B) [Hereditary B] : closure A ≤ B

theorem MisereGames.Form.Hereditary.closure_le {G : Type (u + 1)} [Form G] {A B : G → Prop} [Hereditary B] : closure A ≤ B ↔ A ≤ B

theorem MisereGames.Form.Hereditary.closure_mono {G : Type (u + 1)} [Form G] {A B : G → Prop} (hAB : A ≤ B) : closure A ≤ closure B

theorem MisereGames.Form.ClosedUnderNeg.sInf_closed {G : Type (u + 1)} [Form G] {S : Set (G → Prop)} (hS : ∀ A ∈ S, ClosedUnderNeg A) : ClosedUnderNeg (sInf S)

@[reducible, inline]

noncomputable abbrev MisereGames.Form.ClosedUnderNeg.closureOperator {G : Type (u + 1)} [Form G] : ClosureOperator (G → Prop)

The closure operator for finding the smallest conjugate closed set containing the given set.

Equations

• MisereGames.Form.ClosedUnderNeg.closureOperator = ClosureOperator.ofCompletePred (fun (A : G → Prop) => MisereGames.Form.ClosedUnderNeg A) ⋯

@[reducible, inline]

noncomputable abbrev MisereGames.Form.ClosedUnderNeg.closure {G : Type (u + 1)} [Form G] (A : G → Prop) : G → Prop

The conjugate closure of a given set.

Equations

• MisereGames.Form.ClosedUnderNeg.closure A = MisereGames.Form.ClosedUnderNeg.closureOperator A

theorem MisereGames.Form.ClosedUnderNeg.subset_closure {G : Type (u + 1)} [Form G] (A : G → Prop) : A ≤ closure A

theorem MisereGames.Form.ClosedUnderNeg.mem_closure_of_mem {G : Type (u + 1)} [Form G] {A : G → Prop} {g : G} (hg : A g) : closure A g

instance MisereGames.Form.ClosedUnderNeg.closure_closed {G : Type (u + 1)} [Form G] (A : G → Prop) : ClosedUnderNeg (closure A)

theorem MisereGames.Form.ClosedUnderNeg.neg_mem_closure {G : Type (u + 1)} [Form G] {A : G → Prop} {g : G} (hg : closure A g) : closure A (-g)

theorem MisereGames.Form.ClosedUnderNeg.closure_min {G : Type (u + 1)} [Form G] {A B : G → Prop} (hAB : A ≤ B) [ClosedUnderNeg B] : closure A ≤ B

theorem MisereGames.Form.ClosedUnderNeg.closure_le {G : Type (u + 1)} [Form G] {A B : G → Prop} [ClosedUnderNeg B] : closure A ≤ B ↔ A ≤ B

theorem MisereGames.Form.ClosedUnderNeg.closure_mono {G : Type (u + 1)} [Form G] {A B : G → Prop} (hAB : A ≤ B) : closure A ≤ closure B

theorem MisereGames.ClosedUnderDicotic.sInf_closed {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) {S : Set (G → Prop)} (hS : ∀ A ∈ S, ClosedUnderDicotic IsAmbient A) : ClosedUnderDicotic IsAmbient (sInf S)

@[reducible, inline]

noncomputable abbrev MisereGames.ClosedUnderDicotic.closureOperator {G : Type (u + 1)} [Form G] (IsAmbient : G → Prop) : ClosureOperator (G → Prop)

The closure operator for finding the smallest dicotically closed set (given the ambient context) containing the given set.

Equations

• MisereGames.ClosedUnderDicotic.closureOperator IsAmbient = ClosureOperator.ofCompletePred (fun (A : G → Prop) => MisereGames.ClosedUnderDicotic IsAmbient A) ⋯

@[reducible, inline]

noncomputable abbrev MisereGames.ClosedUnderDicotic.closure {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : G → Prop

The dicotic closure (within the ambient context) of a given set.

Equations

• MisereGames.ClosedUnderDicotic.closure IsAmbient A = (MisereGames.ClosedUnderDicotic.closureOperator IsAmbient) A

theorem MisereGames.ClosedUnderDicotic.subset_closure {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : A ≤ closure IsAmbient A

theorem MisereGames.ClosedUnderDicotic.mem_closure_of_mem {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} {g : G} (hg : A g) : closure IsAmbient A g

instance MisereGames.ClosedUnderDicotic.closure_closed {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : ClosedUnderDicotic IsAmbient (closure IsAmbient A)

theorem MisereGames.ClosedUnderDicotic.dicotic_mem_closure {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} (B C : Set G) [Small.{u, u + 1} ↑B] [Small.{u, u + 1} ↑C] (hB : ∀ b ∈ B, closure IsAmbient A b) (hC : ∀ c ∈ C, closure IsAmbient A c) (hBne : B.Nonempty) (hCne : C.Nonempty) (hAmbient : IsAmbient !{B | C}) : closure IsAmbient A !{B | C}

theorem MisereGames.ClosedUnderDicotic.closure_min {G : Type (u + 1)} [Form G] {IsAmbient A B : G → Prop} (hAB : A ≤ B) [ClosedUnderDicotic IsAmbient B] : closure IsAmbient A ≤ B

theorem MisereGames.ClosedUnderDicotic.closure_le {G : Type (u + 1)} [Form G] {IsAmbient A B : G → Prop} [ClosedUnderDicotic IsAmbient B] : closure IsAmbient A ≤ B ↔ A ≤ B

theorem MisereGames.ClosedUnderDicotic.closure_mono {G : Type (u + 1)} [Form G] {IsAmbient A B : G → Prop} (hAB : A ≤ B) : closure IsAmbient A ≤ closure IsAmbient B