Scarf's combinatorial lemma

This file develops the combinatorial core behind Scarf's lemma. It introduces the IndexedLOrder class of families of linear orders indexed by a finite set, the notions of dominant sets, cells, rooms and doors, and the colorful/nearly-colorful machinery used in the parity (door-counting) argument that culminates in IndexedLOrder.Scarf: every coloring of a finite indexed linear order admits a colorful room.

theorem injOn_sdiff {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (s : Finset α) (f : α → β) (h : s.card = (Finset.image f s).card + 1) : ∃ (a : α) (b : α), 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.

• IST : I → LinearOrder T

  The linear order on T at index i.

@[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 := ⋯ }

@[reducible, inline]

abbrev IndexedLOrder.ltAt {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (i : I) (a b : T) : Prop

Strict order at index i for an IndexedLOrder: lt a b for the linear order IST i.

Equations

• IndexedLOrder.ltAt i a b = (a < b)

@[reducible, inline]

abbrev IndexedLOrder.leAt {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (i : I) (a b : T) : Prop

Non-strict order at index i for an IndexedLOrder: le a b for the linear order IST i.

Equations

• IndexedLOrder.leAt i a b = (a ≤ b)

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

σ is dominant for C: every point is dominated at some index of C.

Equations

• IndexedLOrder.isDominant σ C = ∀ (y : T), ∃ i ∈ C, ∀ x ∈ σ, IndexedLOrder.leAt i 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

The minimum of σ in the linear order at index i.

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

A cell: σ is dominant for 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

A room: a cell whose color and goods sets have equal size.

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

A door: a cell whose color set is one larger than its goods set.

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

The relation that one cell is a door of another room.

• 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

An outside door: a door whose goods part is empty.

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

An internal door: a door that is not an outside door.

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.mSet {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (τ : Finset T) (D : Finset I) (i : I) (h_nonempty : τ.Nonempty) : Set T

The set of points maximizing the dominance condition at a missing index.

Equations

• IndexedLOrder.mSet τ D i h_nonempty = {y : T | ∀ k ∈ D, k ≠ i → IndexedLOrder.ltAt k (IndexedLOrder.mini h_nonempty k) y}

def IndexedLOrder.isMaximalInMSet {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

m is maximal in the mSet of the given data.

Equations

• IndexedLOrder.isMaximalInMSet τ D i h_nonempty x = (x ∈ IndexedLOrder.mSet τ D i h_nonempty ∧ ∀ y ∈ IndexedLOrder.mSet τ D i h_nonempty, IndexedLOrder.leAt i y x)

noncomputable def IndexedLOrder.mElement {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 : (mSet τ D i h_nonempty).Nonempty) : T

A chosen maximal element of the mSet.

Equations

• IndexedLOrder.mElement τ D i h_nonempty h = (IndexedLOrder.mSet τ 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 : (mSet τ D i h_nonempty).Nonempty) : isMaximalInMSet τ D i h_nonempty (mElement τ D i h_nonempty h)

theorem IndexedLOrder.sublemma_3_1 {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq I] (τ : 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) ∧ mSet τ 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] (τ : 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}, (mSet τ D i h_nonempty).Nonempty ∧ isMaximalInMSet τ D i h_nonempty x

theorem IndexedLOrder.M_sets_disjoint {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I 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) : mSet τ D a h_nonempty ∩ mSet τ D b h_nonempty = ∅

theorem IndexedLOrder.m_element_not_in_tau {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [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 : (mSet τ D i h_nonempty).Nonempty) (h_i_is : i = a ∨ i = b) : mElement τ 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 I] (τ : 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 : (mSet τ D i h_nonempty).Nonempty) (x : T) (h_x_max : isMaximalInMSet τ D i h_nonempty x) : x = mElement τ 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] [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 : (mSet τ D a h_nonempty).Nonempty) (h_Mb_nonempty : (mSet τ D b h_nonempty).Nonempty) (x : T) (h_room : isRoom (insert x τ) D) (hx_not_mem : x ∉ τ) : x = mElement τ D a h_nonempty h_Ma_nonempty ∨ x = mElement τ D b h_nonempty h_Mb_nonempty

theorem IndexedLOrder.internalDoorTwoRoomsBothNonempty {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] [Finite T] (τ : Finset T) (D : Finset I) (h_door : isDoor τ D) (h_nonempty : τ.Nonempty) (a b : I) (ha_mem : a ∈ D) (hb_mem : b ∈ D) (h_eq_mini : mini h_nonempty a = mini h_nonempty b) (hab : a ≠ b) (h_card : D.card = τ.card + 1) (h_disjoint : mSet τ D a h_nonempty ∩ mSet τ D b h_nonempty = ∅) (h_Ma_nonempty : (mSet τ D a h_nonempty).Nonempty) (h_Mb_nonempty : (mSet τ D b h_nonempty).Nonempty) : ∃ (σ₁ : 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₂

Two-rooms conclusion when both mSets are nonempty.

theorem IndexedLOrder.internalDoorTwoRoomsLeftEmpty {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] [Finite T] (τ : Finset T) (D : Finset I) (h_door : isDoor τ D) (h_nonempty : τ.Nonempty) (a b : I) (ha_mem : a ∈ D) (hb_mem : b ∈ D) (h_eq_mini : mini h_nonempty a = mini h_nonempty b) (hab : a ≠ b) (h_card : D.card = τ.card + 1) (h_disjoint : mSet τ D a h_nonempty ∩ mSet τ D b h_nonempty = ∅) (h_Ma_empty : mSet τ D a h_nonempty = ∅) (h_Mb_nonempty : (mSet τ D b h_nonempty).Nonempty) : ∃ (σ₁ : 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₂

Two-rooms conclusion when the first mSet is empty but the second is nonempty.

theorem IndexedLOrder.internalDoorTwoRoomsRightEmpty {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] [Finite T] (τ : Finset T) (D : Finset I) (h_door : isDoor τ D) (h_nonempty : τ.Nonempty) (a b : I) (ha_mem : a ∈ D) (hb_mem : b ∈ D) (h_eq_mini : mini h_nonempty a = mini h_nonempty b) (hab : a ≠ b) (h_card : D.card = τ.card + 1) (h_Ma_nonempty : (mSet τ D a h_nonempty).Nonempty) (h_Mb_nonempty : ¬(mSet τ D b h_nonempty).Nonempty) : ∃ (σ₁ : 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₂

Two-rooms conclusion when the first mSet is nonempty but the second is empty.

theorem IndexedLOrder.internal_door_two_rooms {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [DecidableEq T] [DecidableEq I] [Finite 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

A colorful cell: the image of the coloring on σ equals 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

A nearly colorful cell: exactly one color of C is missing.

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

A nearly colorful cell whose missing color is exactly i.

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 {α : Type u_3} {s : Finset α} {a : α} (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.pickColorfulPoint {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) : ↥σ

A chosen point of the goods set of a colorful room.

Equations

• IndexedLOrder.pickColorfulPoint 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)

The set of nearly colorful doors of a given room.

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] (σ : 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.doorsOfNCroomInjective {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) (h_eq : σ.card = (Finset.image c σ).card) : ∃ (door1 : Finset T × Finset I) (door2 : Finset T × Finset I), door1 ≠ door2 ∧ NCdoors c σ C = {door1, door2}

The two doors of a nearly colorful room, when the coloring is injective on σ.

theorem IndexedLOrder.pairEqOfCollision {T : Type u_1} {I : Type u_2} [DecidableEq I] {c : T → I} {σ : Finset T} [DecidableEq T] {x y a b : T} (h_x_in_σ : x ∈ σ) (h_y_in_σ : y ∈ σ) (h_xy_ne : x ≠ y) (h_cxy_eq : c x = c y) (ha_in_σ : a ∈ σ) (hb_in_σ : b ∈ σ) (hc_eq : c a = c b) (hab_ne : a ≠ b) (h_inj_outside : Set.InjOn c (↑σ \ {a, b})) (h_inj : σ.card = (Finset.image c σ).card + 1) : {x, y} = {a, b}

The unordered colliding pair equals {x, y} for a repeated coloring.

theorem IndexedLOrder.collisionPairEq {T : Type u_1} {I : Type u_2} [DecidableEq I] {c : T → I} {σ : Finset T} {x y a b : T} (h_x_in_σ : x ∈ σ) (h_y_in_σ : y ∈ σ) (h_xy_ne : x ≠ y) (h_cxy_eq : c x = c y) (ha_in_σ : a ∈ σ) (hb_in_σ : b ∈ σ) (hc_eq : c a = c b) (hab_ne : a ≠ b) (h_inj_outside : Set.InjOn c (↑σ \ {a, b})) (h_inj : σ.card = (Finset.image c σ).card + 1) : a = x ∧ b = y ∨ a = y ∧ b = x

The colliding pair {a, b} of a repeated coloring coincides with {x, y}.

theorem IndexedLOrder.uniqueMissingColor {T : Type u_1} {I : Type u_2} [DecidableEq I] {c : T → I} {σ : Finset T} {C : Finset I} (h_missing_card : (C \ Finset.image c σ).card = 1) : ∃! i₀ : I, i₀ ∈ C ∧ i₀ ∉ Finset.image c σ

A nearly colorful room has a unique missing color in C.

theorem IndexedLOrder.doorsOfNCroomRepeated {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) (h_inj : σ.card = (Finset.image c σ).card + 1) : ∃ (door1 : Finset T × Finset I) (door2 : Finset T × Finset I), door1 ≠ door2 ∧ NCdoors c σ C = {door1, door2}

The two doors of a nearly colorful room, when one color of σ is repeated.

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)

The finset of colorful rooms of a coloring.

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)

The set used for the double-counting parity argument of typed doors.

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 {α : Type u_3} (s : Finset α) (p : α → 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 I] (c : T → I) [Fintype T] [Fintype I] [Inhabited I] : (colorful c).Nonempty