EconCSLib.Math.FixedPoint.Scarf

Scarf's combinatorial lemma: every coloring of a finite type admits a colorful room.

Scarf's lemma is a combinatorial fixed-point theorem that generalises Sperner's lemma from simplicial complexes to the more abstract setting of indexed linear orders. It is the combinatorial engine behind the proof of Brouwer's fixed-point theorem for the standard simplex (EconCSLib.Math.FixedPoint.Brouwer).

Setup

We work with two types:

• T — a finite inhabited type whose elements play the role of vertices (or lattice points).
• I — a finite type whose elements play the role of coordinate directions (or colors).

An IndexedLOrder I T is a family of linear orders on T, one for each i : I. Write x ≤[i] y for the order at index i.

A finite set σ : Finset T is dominant with respect to C : Finset I (isDominant σ C) if every element y : T has, for some i ∈ C, a minimum in σ that is ≤[i] y. Dominance is the key invariant: it generalises the notion of a simplex containing a given point in its convex hull.

Key definitions

• IndexedLOrder I T — typeclass: a family I → LinearOrder T of linear orders on T.
• isDominant σ C — σ dominates every point of T using some order from C.
• isRoom σ C — dominant cell with |σ| = |C| (a "full-rank" cell).
• isDoor σ C — dominant cell with |C| = |σ| + 1 (one surplus color).
• isColorful c σ C — room where the coloring c : T → I maps σ bijectively onto C.
• colorful c — the Finset of all colorful rooms (σ, C).

Main result

• Scarf — for any coloring c : T → I (with [Inhabited I]), IST.colorful c is nonempty: there exists a colorful room (σ, C).

Proof strategy

The proof uses a parity argument on a bipartite counting set:

1. Define a double-counting set dbcountingset c i pairing each nearly-colorful room with its adjacent colorful and outside-door rooms.
2. Show that the number of typed nearly-colorful rooms of each type is odd (typed_colorful_room_odd), using an induction that tracks inside/outside doors.
3. Since an odd number is positive, the set of colorful rooms is nonempty.

References

• Scarf, H. E., "The Core of an N Person Game", Econometrica 35 (1967), pp. 50–69.
• Scarf, H. E., "The Computation of Economic Equilibria", Yale University Press, 1973.
• Shapley, L. S., "On Balanced Games Without Side Payments", in Mathematical Programming (1973), pp. 261–290.

theorem injOn_sdiff {X : Type u} {Y : Type v} [DecidableEq X] [DecidableEq Y] (s : Finset X) (f : X → Y) (h : s.card = (Finset.image f s).card + 1) : ∃ (a : X) (b : X), a ∈ s ∧ b ∈ s ∧ f a = f b ∧ a ≠ b ∧ Set.InjOn f (↑s \ ↑{a, b})

class IndexedLOrder (I : Type u_3) (T : Type u_4) : Type (max u_3 u_4)

A family of linear orders on T indexed by I.

Each i : I provides a linear order IST i : LinearOrder T on the type T. This is the abstract setting for Scarf's lemma: the index set I plays the role of coordinate directions, and the orders encode how each direction ranks the points of T.

• IST : I → LinearOrder T

@[implicit_reducible]

instance instFunLikeIndexedLOrderLinearOrder {T : Type u_1} {I : Type u_2} : FunLike (IndexedLOrder I T) I (LinearOrder T)

Equations

• instFunLikeIndexedLOrderLinearOrder = { coe := fun (a : IndexedLOrder I T) => IndexedLOrder.IST, coe_injective' := ⋯ }

def IndexedLOrder.isDominant {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (σ : Finset T) (C : Finset I) : Prop

σ is dominant with respect to C: for every y : T there exists i ∈ C such that every element of σ is ≥[i] y — i.e., σ contains, in the order at i, a minimum that dominates y.

This is the key structural invariant of Scarf's lemma. It generalises the notion that a simplex vertex set "covers" a given point in its convex hull.

Equations

• IndexedLOrder.isDominant σ C = ∀ (y : T), ∃ i ∈ C, ∀ x ∈ σ, y ≤ x

theorem IndexedLOrder.Nonempty_of_Dominant {T : Type u_1} [Inhabited T] {I : Type u_2} [IST : IndexedLOrder I T] {σ : Finset T} {C : Finset I} (h : isDominant σ C) : C.Nonempty

theorem IndexedLOrder.Dominant_of_subset {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (σ τ : Finset T) (C : Finset I) : τ ⊆ σ → isDominant σ C → isDominant τ C

theorem IndexedLOrder.Dominant_of_supset {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (σ : Finset T) (C D : Finset I) : C ⊆ D → isDominant σ C → isDominant σ D

@[reducible, inline]

abbrev IndexedLOrder.mini {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] {σ : Finset T} (h2 : σ.Nonempty) (i : I) : T

Equations

• IndexedLOrder.mini h2 i = σ.min' h2

theorem IndexedLOrder.keylemma_of_dominant {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] {σ : Finset T} {C : Finset I} (h1 : isDominant σ C) (h2 : σ.Nonempty) : σ = Finset.image (mini h2) C

theorem IndexedLOrder.card_le_of_domiant {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] {σ : Finset T} {C : Finset I} (h1 : isDominant σ C) : σ.card ≤ C.card

theorem IndexedLOrder.empty_Dominant {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] {D : Finset I} (h : D.Nonempty) : isDominant Finset.empty D

@[reducible, inline]

abbrev IndexedLOrder.isCell {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (σ : Finset T) (C : Finset I) : Prop

Alias for isDominant σ C: the cell predicate for the pair (σ, C).

Equations

• IndexedLOrder.isCell σ C = IndexedLOrder.isDominant σ C

@[reducible, inline]

abbrev IndexedLOrder.isRoom {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (σ : Finset T) (C : Finset I) : Prop

(σ, C) is a room: a dominant cell with |σ| = |C|.

In a room, the index set and the point set have the same cardinality. Colorful rooms (where the coloring maps σ bijectively onto C) are rooms.

Equations

• IndexedLOrder.isRoom σ C = (IndexedLOrder.isCell σ C ∧ C.card = σ.card)

theorem IndexedLOrder.sigma_nonempty_of_room {T : Type u_1} [Inhabited T] {I : Type u_2} [IST : IndexedLOrder I T] {σ : Finset T} {C : Finset I} (h : isRoom σ C) : σ.Nonempty

@[reducible, inline]

abbrev IndexedLOrder.isDoor {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (σ : Finset T) (C : Finset I) : Prop

(σ, C) is a door: a dominant cell with |C| = |σ| + 1.

A door has one more color than points; it is adjacent to exactly two rooms in the Scarf complex. Doors are the "walls" between rooms in the parity argument.

Equations

• IndexedLOrder.isDoor σ C = (IndexedLOrder.isCell σ C ∧ C.card = σ.card + 1)

inductive IndexedLOrder.isDoorof {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] (τ : Finset T) (D : Finset I) (σ : Finset T) (C : Finset I) : Prop

• idoor {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] {τ : Finset T} {D : Finset I} {σ : Finset T} {C : Finset I} (h0 : isCell σ C) (h1 : isDoor τ D) (x : T) : x ∉ τ → ∀ (h2 : insert x τ = σ) (h3 : D = C), isDoorof τ D σ C
• odoor {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] {τ : Finset T} {D : Finset I} {σ : Finset T} {C : Finset I} (h0 : isCell σ C) (h1 : isDoor τ D) (j : I) : j ∉ C → ∀ (h2 : τ = σ) (h3 : D = insert j C), isDoorof τ D σ C

theorem IndexedLOrder.isCell_of_door {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (σ : Finset T) (C : Finset I) [DecidableEq T] [DecidableEq I] {τ : Finset T} {D : Finset I} (h1 : isDoorof τ D σ C) : isCell τ D

theorem IndexedLOrder.isRoom_of_Door {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] {σ : Finset T} {C : Finset I} [DecidableEq T] [DecidableEq I] {τ : Finset T} {D : Finset I} (h1 : isDoorof τ D σ C) : isRoom σ C

theorem IndexedLOrder.room_is_not_door {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (σ : Finset T) (C : Finset I) [DecidableEq T] [DecidableEq I] (h1 : isRoom σ C) (τ : Finset T) (D : Finset I) : ¬isDoorof σ C τ D

@[reducible, inline]

abbrev IndexedLOrder.isOutsideDoor {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (τ : Finset T) (D : Finset I) : Prop

Equations

• IndexedLOrder.isOutsideDoor τ D = (IndexedLOrder.isDoor τ D ∧ τ = Finset.empty)

@[reducible, inline]

abbrev IndexedLOrder.isInternalDoor {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (τ : Finset T) (D : Finset I) : Prop

Equations

• IndexedLOrder.isInternalDoor τ D = (IndexedLOrder.isDoor τ D ∧ τ.Nonempty)

theorem IndexedLOrder.outsidedoor_singleton {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (i : I) : isOutsideDoor Finset.empty {i}

theorem IndexedLOrder.outsidedoor_is_singleton {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] {τ : Finset T} {D : Finset I} (h : isOutsideDoor τ D) : τ = Finset.empty ∧ ∃ (i : I), D = {i}

def IndexedLOrder.M_set {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (τ : Finset T) (D : Finset I) (i : I) (h_nonempty : τ.Nonempty) : Set T

Equations

• IndexedLOrder.M_set τ D i h_nonempty = {y : T | ∀ k ∈ D, k ≠ i → IndexedLOrder.mini h_nonempty k < y}

def IndexedLOrder.is_maximal_in_M_set {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (τ : Finset T) (D : Finset I) (i : I) (h_nonempty : τ.Nonempty) (x : T) : Prop

Equations

• IndexedLOrder.is_maximal_in_M_set τ D i h_nonempty x = (x ∈ IndexedLOrder.M_set τ D i h_nonempty ∧ ∀ y ∈ IndexedLOrder.M_set τ D i h_nonempty, y ≤ x)

noncomputable def IndexedLOrder.m_element {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [Fintype T] (τ : Finset T) (D : Finset I) (i : I) (h_nonempty : τ.Nonempty) (h : (M_set τ D i h_nonempty).Nonempty) : T

Equations

• IndexedLOrder.m_element τ D i h_nonempty h = (IndexedLOrder.M_set τ D i h_nonempty).toFinset.max' ⋯

theorem IndexedLOrder.m_element_is_maximal {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [Fintype T] (τ : Finset T) (D : Finset I) (i : I) (h_nonempty : τ.Nonempty) (h : (M_set τ D i h_nonempty).Nonempty) : is_maximal_in_M_set τ D i h_nonempty (m_element τ D i h_nonempty h)

theorem IndexedLOrder.sublemma_3_1 {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] [Fintype T] (τ : Finset T) (D : Finset I) (h_door : isDoor τ D) (h_nonempty : τ.Nonempty) (i : I) : i ∈ D → (isDominant τ (D.erase i) ↔ ∃ (a : I) (b : I), a ∈ D ∧ b ∈ D ∧ a ≠ b ∧ mini h_nonempty a = mini h_nonempty b ∧ (i = a ∨ i = b) ∧ M_set τ D i h_nonempty = ∅)

theorem IndexedLOrder.sublemma_3_2 {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] [Fintype T] (τ : Finset T) (D : Finset I) (x : T) (h_door : isDoor τ D) (h_nonempty : τ.Nonempty) (h_not_mem : x ∉ τ) (a b : I) (ha : a ∈ D) (hb : b ∈ D) (hab : a ≠ b) (h_eq : mini h_nonempty a = mini h_nonempty b) : isDominant (insert x τ) D ↔ ∃ i ∈ {a, b}, (M_set τ D i h_nonempty).Nonempty ∧ is_maximal_in_M_set τ D i h_nonempty x

theorem IndexedLOrder.M_sets_disjoint {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] [Fintype T] (τ : Finset T) (D : Finset I) (a b : I) (h_nonempty : τ.Nonempty) (h_door : isDoor τ D) (ha : a ∈ D) (hb : b ∈ D) (hab : a ≠ b) (h_eq : mini h_nonempty a = mini h_nonempty b) : M_set τ D a h_nonempty ∩ M_set τ D b h_nonempty = ∅

theorem IndexedLOrder.m_element_not_in_tau {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] [Fintype T] (τ : Finset T) (D : Finset I) (i a b : I) (h_door : isDoor τ D) (h_nonempty : τ.Nonempty) (ha_mem : a ∈ D) (hb_mem : b ∈ D) (hab : a ≠ b) (h_eq_mini : mini h_nonempty a = mini h_nonempty b) (h_M_nonempty : (M_set τ D i h_nonempty).Nonempty) (h_i_is : i = a ∨ i = b) : m_element τ D i h_nonempty h_M_nonempty ∉ τ

theorem IndexedLOrder.odoor_index_in_pair {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] [Fintype T] (τ : Finset T) (D C : Finset I) (a b j : I) (_h_door : isDoor τ D) (h_nonempty : τ.Nonempty) (ha_mem : a ∈ D) (hb_mem : b ∈ D) (hab : a ≠ b) (h_eq_mini : mini h_nonempty a = mini h_nonempty b) (h_dom : isDominant τ C) (h_room_card : C.card = τ.card) (_hj_not_mem : j ∉ C) (hc_eq : D = insert j C) : j ∈ {a, b}

theorem IndexedLOrder.maximal_element_unique {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [Fintype T] (τ : Finset T) (D : Finset I) (i : I) (h_nonempty : τ.Nonempty) (h_M_nonempty : (M_set τ D i h_nonempty).Nonempty) (x : T) (h_x_max : is_maximal_in_M_set τ D i h_nonempty x) : x = m_element τ D i h_nonempty h_M_nonempty

theorem IndexedLOrder.idoor_determines_element {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] [Fintype T] (τ : Finset T) (D : Finset I) (a b : I) (h_door : isDoor τ D) (h_nonempty : τ.Nonempty) (ha_mem : a ∈ D) (hb_mem : b ∈ D) (hab : a ≠ b) (h_eq_mini : mini h_nonempty a = mini h_nonempty b) (h_Ma_nonempty : (M_set τ D a h_nonempty).Nonempty) (h_Mb_nonempty : (M_set τ D b h_nonempty).Nonempty) (x : T) (h_room : isRoom (insert x τ) D) (hx_not_mem : x ∉ τ) : x = m_element τ D a h_nonempty h_Ma_nonempty ∨ x = m_element τ D b h_nonempty h_Mb_nonempty

theorem IndexedLOrder.internal_door_two_rooms {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] [Fintype T] (τ : Finset T) (D : Finset I) (h_int_door : isInternalDoor τ D) : ∃ (σ₁ : Finset T) (σ₂ : Finset T) (C₁ : Finset I) (C₂ : Finset I), (σ₁, C₁) ≠ (σ₂, C₂) ∧ isRoom σ₁ C₁ ∧ isRoom σ₂ C₂ ∧ isDoorof τ D σ₁ C₁ ∧ isDoorof τ D σ₂ C₂ ∧ ∀ (σ : Finset T) (C : Finset I), isRoom σ C → isDoorof τ D σ C → σ = σ₁ ∧ C = C₁ ∨ σ = σ₂ ∧ C = C₂

def IndexedLOrder.isColorful {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] (c : T → I) (σ : Finset T) (C : Finset I) : Prop

(σ, C) is colorful under coloring c : T → I: it is a dominant cell and the coloring c maps σ bijectively onto C (i.e., σ.image c = C).

A colorful room is the central object of Scarf's lemma: its existence is guaranteed for every coloring c.

Equations

• IndexedLOrder.isColorful c σ C = (IndexedLOrder.isCell σ C ∧ Finset.image c σ = C)

def IndexedLOrder.isNearlyColorful {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] (c : T → I) (σ : Finset T) (C : Finset I) : Prop

(σ, C) is nearly colorful: a dominant cell where exactly one color in C is missing from the image of c on σ.

Equations

• IndexedLOrder.isNearlyColorful c σ C = (IndexedLOrder.isCell σ C ∧ (C \ Finset.image c σ).card = 1)

def IndexedLOrder.isTypedNC {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] (c : T → I) (i : I) (σ : Finset T) (C : Finset I) : Prop

(σ, C) is a typed nearly-colorful cell of type i: a dominant cell where i is the unique color in C missing from σ.image c.

Equations

• IndexedLOrder.isTypedNC c i σ C = (IndexedLOrder.isCell σ C ∧ C \ Finset.image c σ = {i})

theorem IndexedLOrder.not_colorful_of_TypedNC {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} {i : I} (h1 : isTypedNC c i σ C) : ¬isColorful c σ C

theorem IndexedLOrder.NC_of_TNC {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} {i : I} (h1 : isTypedNC c i σ C) : isNearlyColorful c σ C

theorem IndexedLOrder.Finset.eq_of_mem_of_card_one {X : Type u_3} [DecidableEq X] {s : Finset X} {a : X} (h_mem : a ∈ s) (h_card : s.card = 1) : s = {a}

theorem IndexedLOrder.room_of_colorful {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} (h : isColorful c σ C) : isRoom σ C

noncomputable def IndexedLOrder.pick_colorful_point {T : Type u_1} [Inhabited T] {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} (h : isColorful c σ C) : ↥σ

Equations

• IndexedLOrder.pick_colorful_point h = Classical.choice ⋯

theorem IndexedLOrder.NC_of_outsidedoor {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} (h : isOutsideDoor σ C) : isNearlyColorful c σ C

theorem IndexedLOrder.NC_or_C_of_door {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} {i : I} {τ : Finset T} {D : Finset I} (h1 : isTypedNC c i τ D) (h2 : isDoorof τ D σ C) : isTypedNC c i σ C ∨ isColorful c σ C

theorem IndexedLOrder.NCtype_of_door {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} {i : I} {τ : Finset T} {D : Finset I} (h1 : isTypedNC c i τ D) : isDoorof τ D σ C → isTypedNC c i σ C → isTypedNC c i τ D

theorem IndexedLOrder.isTypedNC_of_isNearlyColorful_of_isDoorof_isTypedNC {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} {τ : Finset T} {D : Finset I} {i : I} (h_nc : isNearlyColorful c τ D) (h_door : isDoorof τ D σ C) (h_room_typed : isTypedNC c i σ C) : isTypedNC c i τ D

theorem IndexedLOrder.card_of_NCcell {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] {c : T → I} {σ : Finset T} {D : Finset I} (h : isNearlyColorful c σ D) : σ.card = (Finset.image c σ).card ∨ σ.card = (Finset.image c σ).card + 1

theorem IndexedLOrder.image_subset_of_NCdoor {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} (h1 : isNearlyColorful c σ C) (h2 : isDoor σ C) : Finset.image c σ ⊆ C

theorem IndexedLOrder.image_erase_eq_erase_image_of_unique {T : Type u_3} {I : Type u_4} [DecidableEq T] [DecidableEq I] (σ : Finset T) (c : T → I) {z : T} : z ∈ σ → ∀ (uniq : ∀ ⦃w : T⦄, w ∈ σ → c w = c z → w = z), Finset.image c (σ.erase z) = (Finset.image c σ).erase (c z)

@[reducible, inline]

abbrev IndexedLOrder.NCdoors {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] (c : T → I) (σ : Finset T) (C : Finset I) : Set (Finset T × Finset I)

Equations

• IndexedLOrder.NCdoors c σ C = {(τ, D) : Finset T × Finset I | IndexedLOrder.isNearlyColorful c τ D ∧ IndexedLOrder.isDoorof τ D σ C}

theorem IndexedLOrder.three_collision_card_bound {T : Type u_1} {I : Type u_2} [DecidableEq I] [DecidableEq T] (σ : Finset T) (c : T → I) (a b z : T) (ha_in_σ : a ∈ σ) (hb_in_σ : b ∈ σ) (hz_in_σ : z ∈ σ) (hab_ne : a ≠ b) (haz_ne : a ≠ z) (hbz_ne : b ≠ z) (hc_eq : c a = c b) (hcz_eq : c b = c z) : σ.card ≥ (Finset.image c σ).card + 2

theorem IndexedLOrder.image_erase_collision_preserves {T : Type u_1} {I : Type u_2} [DecidableEq I] [DecidableEq T] (σ : Finset T) (c : T → I) (x y : T) (hx_in_σ : x ∈ σ) (hy_in_σ : y ∈ σ) (hxy_ne : x ≠ y) (hcxy_eq : c x = c y) : Finset.image c (σ.erase x) = Finset.image c σ ∧ Finset.image c (σ.erase y) = Finset.image c σ

theorem IndexedLOrder.collision_door_valid {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] [DecidableEq T] (σ : Finset T) (C : Finset I) : ∀ (x : T → I) (x : T) (h_cell : isCell σ C) (hx_in_σ : x ∈ σ) (h_card_eq : C.card = σ.card), isDoorof (σ.erase x) C σ C

theorem IndexedLOrder.doors_of_NCroom {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} [DecidableEq T] (h_room : isRoom σ C) (h_nc : isNearlyColorful c σ C) : ∃ (door1 : Finset T × Finset I) (door2 : Finset T × Finset I), door1 ≠ door2 ∧ NCdoors c σ C = {door1, door2}

@[reducible, inline]

noncomputable abbrev IndexedLOrder.colorful {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] (c : T → I) [Fintype T] [Fintype I] : Finset (Finset T × Finset I)

Equations

• IndexedLOrder.colorful c = {x : Finset T × Finset I | IndexedLOrder.isColorful c x.1 x.2}

@[reducible, inline]

noncomputable abbrev IndexedLOrder.dbcountingset {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] (c : T → I) [Fintype T] [Fintype I] (i : I) : Finset ((Finset T × Finset I) × Finset T × Finset I)

Equations

• IndexedLOrder.dbcountingset c i = {x : (Finset T × Finset I) × Finset T × Finset I | IndexedLOrder.isTypedNC c i x.1.1 x.1.2 ∧ IndexedLOrder.isDoorof x.1.1 x.1.2 x.2.1 x.2.2}

theorem IndexedLOrder.dbcount_outside_door' {T : Type u_1} [Inhabited T] {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] (c : T → I) [Fintype T] [Fintype I] (i : I) : ∃ (x : (Finset T × Finset I) × Finset T × Finset I), {x ∈ dbcountingset c i | isOutsideDoor x.1.1 x.1.2} = {x}

theorem IndexedLOrder.dbcount_outside_door_odd {T : Type u_1} [Inhabited T] {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] (c : T → I) [Fintype T] [Fintype I] (i : I) : Odd {x ∈ dbcountingset c i | isOutsideDoor x.1.1 x.1.2}.card

theorem IndexedLOrder.fiber_size_internal_door {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] [Fintype T] [Fintype I] (c : T → I) (i : I) (y : Finset T × Finset I) (hy_internal : isInternalDoor y.1 y.2) (hy_typed : isTypedNC c i y.1 y.2) : have s := {x ∈ dbcountingset c i | ¬isOutsideDoor x.1.1 x.1.2}; have f := fun (x : (Finset T × Finset I) × Finset T × Finset I) => x.1; {a ∈ s | f a = y}.card = 2

theorem IndexedLOrder.dbcount_internal_door_even {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] (c : T → I) [Fintype T] [Fintype I] (i : I) : Even {x ∈ dbcountingset c i | ¬isOutsideDoor x.1.1 x.1.2}.card

theorem IndexedLOrder.NC_of_NCdoor {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} {i : I} {τ : Finset T} {D : Finset I} (h1 : isTypedNC c i τ D) (h2 : isDoorof τ D σ C) : ¬isColorful c σ C → isTypedNC c i σ C

theorem IndexedLOrder.firber2_doors_NCroom {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} [Fintype T] [Fintype I] {i : I} (h0 : isRoom σ C) (h1 : isTypedNC c i σ C) : {x ∈ dbcountingset c i | x.2 = (σ, C)}.card = 2

theorem IndexedLOrder.dbcount_NCroom {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] (c : T → I) [Fintype T] [Fintype I] (i : I) : Even {x ∈ dbcountingset c i | ¬isColorful c x.2.1 x.2.2}.card

theorem IndexedLOrder.parity_lemma {a b c d : ℕ} (h1 : Odd a) (h2 : Even b) (h3 : Even d) (h4 : a + b = c + d) : Odd c

theorem Finset.card_filter_filter_neg {X : Type u_3} (s : Finset X) (p : X → Prop) [DecidablePred p] : s.card = (filter p s).card + {a ∈ s | ¬p a}.card

theorem IndexedLOrder.typed_colorful_room_odd {T : Type u_1} [Inhabited T] {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] (c : T → I) [Fintype T] [Fintype I] (i : I) : Odd {x ∈ dbcountingset c i | isColorful c x.2.1 x.2.2}.card

theorem IndexedLOrder.Scarf {T : Type u_1} [Inhabited T] {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] (c : T → I) [Fintype T] [Fintype I] [Inhabited I] : (colorful c).Nonempty

Scarf's combinatorial lemma: for any coloring c : T → I and any IndexedLOrder I T, the set of colorful rooms is nonempty.

Proof: parity argument. For any fixed i : I, the number of typed nearly-colorful rooms of type i that appear in dbcountingset c i is odd (typed_colorful_room_odd). In particular it is positive, so a colorful room exists.