Documentation

LeanPool.ErdosTuzaValtr.Config.Mirror

LeanPool.ErdosTuzaValtr.Config.Mirror #

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Config.Mirror.

source
def Config.Mirror {α : Type u_1} [LinearOrder α] (C : Config α) :
Config αᵒᵈ

The mirror configuration on the order dual, obtained by reversing the cup relation.

Equations
Instances For
    source
    @[simp]
    theorem Mirror.cap {α : Type u_1} [LinearOrder α] {C : Config α} {l : List α} :
    C.Mirror.Cap l.Mirror ↔ C.Cap l
    source
    @[simp]
    theorem Mirror.cup {α : Type u_1} [LinearOrder α] {C : Config α} {l : List α} :
    C.Mirror.Cup l.Mirror ↔ C.Cup l
    source
    theorem Mirror.gon {α : Type u_1} [LinearOrder α] {C : Config α} {l1 l2 : List α} :
    C.Mirror.Gon l1.Mirror l2.Mirror ↔ C.Gon l1 l2
    source
    @[simp]
    theorem Mirror.ncap {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} :
    C.Mirror.NCap n l.Mirror ↔ C.NCap n l
    source
    @[simp]
    theorem Mirror.ncup {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l : List α} :
    C.Mirror.NCup n l.Mirror ↔ C.NCup n l
    source
    theorem Mirror.ngon {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {l1 l2 : List α} :
    C.NGon n l1 l2 ↔ C.Mirror.NGon n l1.Mirror l2.Mirror
    source
    @[simp]
    theorem Mirror.hasNCap {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {S : Finset α} :
    C.Mirror.HasNCap n S.Mirror ↔ C.HasNCap n S
    source
    @[simp]
    theorem Mirror.hasNCup {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {S : Finset α} :
    C.Mirror.HasNCup n S.Mirror ↔ C.HasNCup n S
    source
    theorem Mirror.hasNGon {α : Type u_1} [LinearOrder α] {C : Config α} {n : ℕ} {S : Finset α} :
    C.Mirror.HasNGon n S.Mirror ↔ C.HasNGon n S