Documentation

CombinatorialGames.Form.Classes

source
def Form.IsLong {G : Type (u + 1)} :
G → Prop

The ambient space of all games, imposing no restriction. This is the counterpart of IsShort.

Equations
Instances For
    source
    @[simp]
    theorem Form.isLong {G : Type (u + 1)} (g : G) :
    IsLong g
    source
    class Form.HasZero {G : Type (u + 1)} [Form G] (A : G → Prop) :
    Prop
    • has_zero : A 0
    Instances
      source
      class Form.HasNat {G : Type (u + 1)} [Form G] (A : G → Prop) :
      Prop
      • has_nat (n : ℕ) : A ↑n
      Instances
        source
        class Form.HasInt {G : Type (u + 1)} [Form G] (A : G → Prop) :
        Prop
        • has_int (n : ℤ) : A ↑n
        Instances
          source
          instance Form.instHasZeroOfHasNat {G : Type (u + 1)} [Form G] {A : G → Prop} [HasNat A] :
          HasZero A
          source
          instance Form.instHasNatOfHasInt {G : Type (u + 1)} [Form G] {A : G → Prop} [HasInt A] :
          HasNat A
          source
          instance Form.instHasIntIsLong {G : Type (u + 1)} [Form G] :
          HasInt IsLong
          source
          theorem Form.HasInt.has_neg_int {G : Type (u + 1)} [Form G] {A : G → Prop} [HasInt A] (n : ℕ) :
          A (-↑n)
          source
          theorem Form.HasNat.zero {G : Type (u + 1)} [Form G] {A : G → Prop} [HasNat A] :
          A 0
          source
          theorem Form.HasNat.one {G : Type (u + 1)} [Form G] {A : G → Prop} [HasNat A] :
          A 1
          source
          class Form.ClosedUnderAddNat {G : Type (u + 1)} [Form G] (A : G → Prop) :
          Prop
          • has_add {g : G} (h1 : A g) (n : ℕ) : A (g + ↑n)
          Instances
            source
            instance Form.instClosedUnderAddNatIsLong {G : Type (u + 1)} [Form G] :
            ClosedUnderAddNat IsLong
            source
            class Form.ClosedUnderAdd {G : Type (u + 1)} [Form G] (A : G → Prop) :
            Prop
            • has_add (g h : G) (h_g : A g) (h_h : A h) : A (g + h)
            Instances
              source
              instance Form.instClosedUnderAddIsLong {G : Type (u + 1)} [Form G] :
              ClosedUnderAdd IsLong
              source
              class Form.Hereditary {G : Type (u + 1)} [Form G] (A : G → Prop) :
              Prop
              • has_option {g g' : G} (h1 : A g) (h2 : IsOption g' g) : A g'
              Instances
                source
                theorem Form.Hereditary.of_mem_moves {G : Type (u + 1)} [Form G] {A : G → Prop} [Hereditary A] {p : Player} {g g' : G} (hA : A g) (h_mem : g' ∈ moves p g) :
                A g'
                source
                instance Form.instHereditaryIsLong {G : Type (u + 1)} [Form G] :
                Hereditary IsLong
                source
                theorem Form.exists_isZeroLike {G : Type (u + 1)} [Form G] {A : G → Prop} [Hereditary A] (h : ∃ (g : G), A g) :
                ∃ (z : G), A z ∧ IsZeroLike z

                A nonempty hereditary set of forms contains a zero-like form.

                source
                class Form.ClosedUnderNeg {G : Type (u + 1)} [Form G] (A : G → Prop) :
                Prop
                • neg_of {g : G} (h1 : A g) : A (-g)
                Instances
                  source
                  instance Form.instClosedUnderNegIsLong {G : Type (u + 1)} [Form G] :
                  ClosedUnderNeg IsLong
                  source
                  @[simp]
                  theorem Form.ClosedUnderNeg.neg_iff {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderNeg A] {g : G} :
                  A (-g) ↔ A g
                  source
                  theorem Form.HasInt.of_hasNat {G : Type (u + 1)} [Form G] {A : G → Prop} [HasNat A] [ClosedUnderNeg A] :
                  HasInt A
                  source
                  theorem Form.ClosedUnderAddNat.has_add_neg {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAddNat A] [ClosedUnderNeg A] {g : G} (hAg : A g) (n : ℕ) :
                  A (g + -↑n)
                  source
                  theorem Form.ClosedUnderAddNat.has_add_int {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAddNat A] [ClosedUnderNeg A] [HasInt A] {g : G} (hAg : A g) (n : ℤ) :
                  A (g + ↑n)
                  source
                  theorem Form.ClosedUnderAddNat.has_add_int_neg {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAddNat A] [ClosedUnderNeg A] [HasInt A] {g : G} (hAg : A g) (n : ℤ) :
                  A (g + -↑n)