Documentation

CombinatorialGames.SignExpansion.Simplicity

Simplicity relation #

We define the simplicity relation on sign sequences, i.e. the relation where x ≤ y iff x is an initial segment of y. In the literature, this is variously denoted as x ≤ₛ y or x ⊑ y. We also define supremum and infimum operators.

Implementation notes #

Sign sequences already have a linear ordering given by the lexicographic ordering. Since we can't define two separate PartialOrder instances on the same type, we instead create a type alias Simpllicity, and declare the simplicity ordering on that.

For Mathlib #

Type alias #

def Simplicity :

Type (u_1 + 1)

A type alias for SignExpansion, endowed with the simplicity ordering.

Equations

Simplicity = SignExpansion

Instances For

@[implicit_reducible]

noncomputable instance instInhabitedSimplicity :

Inhabited Simplicity

Equations

instInhabitedSimplicity = { default := instInhabitedSimplicity._aux_1 }

def Simplicity.of :

SignExpansion ≃ Simplicity

The identity function between SignExpansion and Simplicity.

Equations

Simplicity.of = Equiv.refl SignExpansion

Instances For

def Simplicity.val :

Simplicity ≃ SignExpansion

The identity function between Simplicity and SignExpansion.

Equations

Simplicity.val = Equiv.refl Simplicity

Instances For

@[simp]

theorem Simplicity.of_val (x : Simplicity) :

of (val x) = x

@[simp]

theorem Simplicity.val_of (x : SignExpansion) :

val (of x) = x

@[implicit_reducible]

instance Simplicity.instBot :

Equations

Simplicity.instBot = { bot := Simplicity.of 0 }

@[simp]

theorem Simplicity.of_zero :

@[simp]

theorem Simplicity.val_bot :

@[implicit_reducible]

instance Simplicity.instFunLikeNatOrdinalSignType :

FunLike Simplicity NatOrdinal SignType

Equations

Simplicity.instFunLikeNatOrdinalSignType = { coe := fun (x : Simplicity) => ⇑(Simplicity.val x), coe_injective := ⋯ }

@[simp]

theorem Simplicity.val_apply (x : Simplicity) (o : NatOrdinal) :

(val x) o = x o

@[simp]

theorem Simplicity.of_apply (x : SignExpansion) (o : NatOrdinal) :

(of x) o = x o

@[simp]

theorem Simplicity.coe_bot :

⇑⊥ = 0

theorem Simplicity.bot_apply (o : NatOrdinal) :

⊥ o = 0

theorem Simplicity.ext {x y : Simplicity} (hxy : ∀ (o : NatOrdinal), x o = y o) :

x = y

theorem Simplicity.ext_iff {x y : Simplicity} :

x = y ↔ ∀ (o : NatOrdinal), x o = y o

def Simplicity.ind {motive : Simplicity → Sort u_1} (of : (a : SignExpansion) → motive (of a)) (a : Simplicity) :

motive a

A recursor for Simplicity. Use as cases x.

Equations

Simplicity.ind of a = of (Simplicity.val a)

Instances For

@[simp]

theorem Simplicity.ind_of {motive : Simplicity → Sort u_2} {of : (a : SignExpansion) → motive (of a)} (a : SignExpansion) :

Simplicity.ind of (Simplicity.of a) = of a

Order instances #

@[implicit_reducible]

instance Simplicity.instPreorder :

Preorder Simplicity

Equations

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

theorem Simplicity.le_def {x y : Simplicity} :

x ≤ y ↔ (val y).restrict (val x).length = val x

theorem Simplicity.of_le_of {x y : SignExpansion} :

of x ≤ of y ↔ y.restrict x.length = x

theorem Simplicity.le_restrict_of_le_of_length_le {x y : Simplicity} {o : WithTop NatOrdinal} (h : x ≤ y) (h' : (val x).length ≤ o) :

x ≤ of ((val y).restrict o)

theorem Simplicity.apply_eq_of_le {x y : Simplicity} {o : NatOrdinal} (h : x ≤ y) (hx : x o ≠ 0) :

x o = y o

theorem Simplicity.le_iff_forall {x y : Simplicity} :

x ≤ y ↔ ∀ (o : NatOrdinal), x o ≠ 0 → x o = y o

theorem Simplicity.le_of_le_of_length_le {x y z : Simplicity} (hx : x ≤ z) (hy : y ≤ z) (h : (val x).length ≤ (val y).length) :

x ≤ y

theorem Simplicity.le_or_ge_of_le {x y z : Simplicity} (hx : x ≤ z) (hy : y ≤ z) :

x ≤ y ∨ y ≤ x

theorem Simplicity.of_restrict_le_of (x : SignExpansion) (o : WithTop NatOrdinal) :

of (x.restrict o) ≤ of x

theorem Simplicity.eq_or_length_lt_of_le {x y : Simplicity} (h : x ≤ y) :

x = y ∨ (val x).length < (val y).length

theorem Simplicity.length_strictMono :

StrictMono fun (x : Simplicity) => (val x).length

@[implicit_reducible]

instance Simplicity.instPartialOrder :

PartialOrder Simplicity

Equations

Simplicity.instPartialOrder = { toPreorder := Simplicity.instPreorder, le_antisymm := ⋯ }

@[implicit_reducible]

instance Simplicity.instOrderBot :

OrderBot Simplicity

Equations

Simplicity.instOrderBot = { toBot := Simplicity.instBot, bot_le := Simplicity.instOrderBot._proof_2 }

Infimum #

@[implicit_reducible]

noncomputable instance Simplicity.instInfSet :

InfSet Simplicity

Equations

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

@[simp]

theorem Simplicity.sInf_empty :

theorem Simplicity.isGLB_sInf_of_nonempty {s : Set Simplicity} (hs : s.Nonempty) :

IsGLB s (sInf s)

@[implicit_reducible]

noncomputable instance Simplicity.instSemilatticeInf :

SemilatticeInf Simplicity

Equations

Simplicity.instSemilatticeInf = SemilatticeInf.ofIsGLB (fun (a b : Simplicity) => sInf {a, b}) Simplicity.instSemilatticeInf._proof_2

theorem Simplicity.sInf_pair (x y : Simplicity) :

sInf {x, y} = x ⊓ y

@[implicit_reducible]

noncomputable instance Simplicity.instCompleteSemilatticeInfWithTop :

CompleteSemilatticeInf (WithTop Simplicity)

Equations

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

Supremum #

@[implicit_reducible]

noncomputable instance Simplicity.instSupSet :

SupSet Simplicity

Equations

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

@[simp]

theorem Simplicity.sSup_empty :

theorem Simplicity.isChain_iff_bddAbove {s : Set Simplicity} :

IsChain (fun (x1 x2 : Simplicity) => x1 ≤ x2) s ↔ BddAbove s

theorem Simplicity.isLUB_sSup_iff_bddAbove {s : Set Simplicity} :

IsLUB s (sSup s) ↔ BddAbove s

theorem Simplicity.isLUB_sSup_of_bddAbove {s : Set Simplicity} :

BddAbove s → IsLUB s (sSup s)

Alias of the reverse direction of Simplicity.isLUB_sSup_iff_bddAbove.

theorem Simplicity.sSup_of_not_bddAbove {s : Set Simplicity} (hs : ¬BddAbove s) :

@[implicit_reducible]

noncomputable instance Simplicity.instMax :

Equations

Simplicity.instMax = { max := fun (x y : Simplicity) => sSup {x, y} }

theorem Simplicity.sSup_pair (x y : Simplicity) :

sSup {x, y} = x ⊔ y

theorem Simplicity.sup_comm (x y : Simplicity) :

x ⊔ y = y ⊔ x

theorem Simplicity.sup_of_le_right {x y : Simplicity} (h : x ≤ y) :

x ⊔ y = y

theorem Simplicity.sup_of_le_left {x y : Simplicity} (h : y ≤ x) :

x ⊔ y = x

theorem Simplicity.directedOn_iff_bddAbove {s : Set Simplicity} :

DirectedOn (fun (x1 x2 : Simplicity) => x1 ≤ x2) s ↔ BddAbove s

@[implicit_reducible]

noncomputable instance Simplicity.instCompletePartialOrder :

CompletePartialOrder Simplicity

Equations

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

@[implicit_reducible]

noncomputable instance Simplicity.instCompleteSemilatticeSupWithTop :

CompleteSemilatticeSup (WithTop Simplicity)

Equations

Simplicity.instCompleteSemilatticeSupWithTop = { toPartialOrder := WithTop.instPartialOrder, toSupSet := WithTop.instSupSet, isLUB_sSup := ⋯ }

@[implicit_reducible]

noncomputable instance Simplicity.instCompleteLatticeWithTop :

CompleteLattice (WithTop Simplicity)

Equations

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

Ordinals #

theorem NatOrdinal.of_toSignExpansion_strictMono :

StrictMono fun (o : NatOrdinal) => Simplicity.of (toSignExpansion o)

@[simp]

theorem NatOrdinal.of_toSignExpansion_le_iff {a b : NatOrdinal} :

Simplicity.of (toSignExpansion a) ≤ Simplicity.of (toSignExpansion b) ↔ a ≤ b

@[simp]

theorem NatOrdinal.of_toSignExpansion_lt_iff {a b : NatOrdinal} :

Simplicity.of (toSignExpansion a) < Simplicity.of (toSignExpansion b) ↔ a < b