LeanPool.ErdosTuzaValtr.Etv.Mirror #
Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Etv.Mirror.
theorem
Mirror.hasLaced
{α : Type u_1}
[LinearOrder α]
{C : Config α}
{n : ℕ}
{S : Finset α}
(p q : α)
:
theorem
Mirror.hasInterweavedLaced
{α : Type u_1}
[LinearOrder α]
{C : Config α}
{n : ℕ}
{S : Finset α}
(p q r s : α)
:
C.Mirror.HasInterweavedLaced n S.Mirror (OrderDual.toDual s) (OrderDual.toDual r) (OrderDual.toDual q)
(OrderDual.toDual p) ↔ C.HasInterweavedLaced n S p q r s