Definitions

def IdentityPattern (n : ℕ) (i j : Fin n) : Prop

Equations

• IdentityPattern n i j = (i = j)

def AllPattern (m n : ℕ) : Fin m → Fin n → Prop

Equations

• AllPattern m n x✝¹ x✝ = True

@[reducible, inline]

abbrev VerticalPattern (m : ℕ) : Fin m → Fin 1 → Prop

Equations

• VerticalPattern m = AllPattern m 1

@[reducible, inline]

abbrev HorizontalPattern (n : ℕ) : Fin 1 → Fin n → Prop

Equations

• HorizontalPattern n = AllPattern 1 n

@[reducible, inline]

abbrev TrivialPattern : Fin 1 → Fin 1 → Prop

Equations

• TrivialPattern = AllPattern 1 1

@[simp]

theorem identityPattern_one : IdentityPattern 1 = TrivialPattern

def HatPattern : Fin 2 → Fin 3 → Prop

Equations

• HatPattern = ![![False, True, False], ![True, False, True]]

Proofs

@[simp]

theorem ex_of_isEmpty {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [IsEmpty α] [IsEmpty β] (P : α → β → Prop) (n : ℕ) : ex P n = 0

@[simp]

theorem ex_trivialPattern (n : ℕ) : ex TrivialPattern n = 0

@[simp]

theorem ex_identityPattern_two (n : ℕ) : ex (IdentityPattern 2) n = 2 * n - 1

theorem ex_verticalPattern_two (n : ℕ) : ex (VerticalPattern 2) n = n

theorem ex_horizontal (k n : ℕ) : ex (HorizontalPattern k) n ≤ n * (k - 1)

theorem ex_vertical (k n : ℕ) : ex (VerticalPattern k) n ≤ n * (k - 1)

theorem ex_hat (n : ℕ) : ex HatPattern n ≤ 3 * n