def L'' : Fin 2 → Fin 2 → Prop

Equations

• L'' = ![![false = true, true = true], ![true = true, true = true]]

def A' : Fin 2 → Fin 1 → Prop

Equations

• A' = ![![true = true], ![false = true]]

def B' : Fin 2 → Fin 1 → Prop

Equations

• B' = ![![false = true], ![true = true]]

@[reducible, inline]

abbrev tranpose {α : Type u_1} {β : Type u_2} (M : α → β → Prop) : β → α → Prop

Equations

• tranpose M x y = M y x

def rev_all_rows {α : Type u_1} {β : Type u_2} (M : α → β → Prop) : α → βᵒᵈ → Prop

Equations

• rev_all_rows M i = M i ∘ ⇑OrderDual.ofDual

def rot_cw {α : Type u_1} {β : Type u_2} (M : α → β → Prop) : β → αᵒᵈ → Prop

Equations

• rot_cw M = (rev_all_rows ∘ tranpose) M

def rev_all_rows_via_list {α : Type u_1} {n : ℕ} (M : α → Fin n → Prop) : α → Fin n → Prop

Equations

• rev_all_rows_via_list M a i = M a i.rev

def L : Fin 2 → Fin 2 → Prop

Equations

• L = ![![true = true, false = true], ![true = true, true = true]]

def L' : Fin 2 → Fin 2 → Prop

Equations

• L' = ![![true = true, true = true], ![true = true, false = true]]

def X : (Fin 3)ᵒᵈ → Bool

Equations

• X = ![true, false, false] ∘ ⇑OrderDual.ofDual

def Y : Fin 3 → Bool

Equations

• Y = ![false, false, true]

def A : Fin 1 → Fin 2 → Prop

Equations

• A = ![![true = true, false = true]]

def B : Fin 1 → (Fin 2)ᵒᵈ → Prop

Equations

• B = ![![true = true, false = true] ∘ ⇑OrderDual.ofDual]

def C : Fin 1 → Fin 2 → Prop

Equations

• C = ![![false = true, true = true]]

def a : Fin 2 → Bool

Equations

• a = ![true, false]

def c : Fin 2 → Bool

Equations

• c = ![false, true]

def b : (Fin 2)ᵒᵈ → Bool

Equations

• b = ![false, true] ∘ ⇑OrderDual.ofDual