instance Pi.Lex.finite {α : Type u_1} {β : α → Type u_2} [DecidableEq α] [Finite α] [∀ (a : α), Finite (β a)] : Finite (Lex ((i : α) → (fun (a : α) => β a) i))

A dependent product of finite, indexed by finite, is a finite.

@[reducible, inline]

abbrev TT (n l : ℕ+) : Set (Lex ((i : Fin ↑n) → (fun (x : Fin ↑n) => Fin (↑l + 1)) i))

Equations

• TT n l = {x : Lex ((i : Fin ↑n) → (fun (x : Fin ↑n) => Fin (↑l + 1)) i) | ∑ i : Fin ↑n, ↑(x i) = ↑l}

instance TT.finite (n l : ℕ+) : Finite ↑(TT n l)

@[instance_reducible]

instance TT.inhabited (n l : ℕ+) : Inhabited ↑(TT n l)

Equations

• TT.inhabited n l = { default := ⟨fun (i : Fin ↑n) => if i = 0 then Fin.last ↑l else 0, ⋯⟩ }

@[instance_reducible]

instance TT.funlike (n l : ℕ+) : FunLike (↑(TT n l)) (Fin ↑n) (Fin (↑l + 1))

Equations

• TT.funlike n l = { coe := fun (a : ↑(TT n l)) => ↑a, coe_injective := ⋯ }

noncomputable def TTtostdSimplex {n l : ℕ+} (x : ↑(TT n l)) : ↑(stdSimplex ℝ (Fin ↑n))

Equations

• TTtostdSimplex x = ⟨fun (i : Fin ↑n) => ↑↑(x i) / ↑↑l, ⋯⟩

@[instance_reducible]

noncomputable instance TT.CoestdSimplex (n l : ℕ+) : CoeOut ↑(TT n l) ↑(stdSimplex ℝ (Fin ↑n))

Equations

• TT.CoestdSimplex n l = { coe := TTtostdSimplex }

@[reducible, inline]

abbrev TT.Ilt {n l : ℕ+} (i : Fin ↑n) (x y : ↑(TT n l)) : Prop

Equations

• TT.Ilt i x y = (toLex (x i, x) < toLex (y i, y))

instance TT.IST (n l : ℕ+) (i : Fin ↑n) : IsStrictTotalOrder (↑(TT n l)) (Ilt i)

@[instance_reducible]

noncomputable instance TT.ILO {n l : ℕ+} : IndexedLOrder (Fin ↑n) ↑(TT n l)

Equations

• TT.ILO = { IST := fun (i : Fin ↑n) => linearOrderOfSTO (TT.Ilt i) }

theorem TT.Ilt_def (n l : ℕ+) (i : Fin ↑n) (a b : ↑(TT n l)) : a < b ↔ Ilt i a b

theorem TT.Ilt_keyprop (n l : ℕ+) (i : Fin ↑n) (a b : ↑(TT n l)) : a i < b i → a < b

theorem size_bound_key (n l : ℕ+) (σ : Finset ↑(TT n l)) (C : Finset (Fin ↑n)) (h : IndexedLOrder.isDominant σ C) (h2 : σ.Nonempty) : ↑l < ∑ k ∈ C, (Finset.image (fun (x : ↑(TT n l)) => ↑(x k)) σ).min' ⋯ + C.card

theorem size_bound_in (n l : ℕ+) (σ : Finset ↑(TT n l)) (C : Finset (Fin ↑n)) (h : IndexedLOrder.isDominant σ C) (x : ↑(TT n l)) : x ∈ σ → ∀ y ∈ σ, ∀ (i : Fin ↑n), |↑↑(x i) - ↑↑(y i)| < 2 * (↑↑n + 1)

theorem size_bound_out (n l : ℕ+) (σ : Finset ↑(TT n l)) (C : Finset (Fin ↑n)) (h : IndexedLOrder.isDominant σ C) (x : ↑(TT n l)) : x ∈ σ → ∀ i ∉ C, ↑↑(x i) < ↑↑n + 1

instance stdSimplex.upidx {n : ℕ+} (x y : ↑(stdSimplex ℝ (Fin ↑n))) : Nonempty ↑{i : Fin ↑n | ↑x i ≤ ↑y i}

noncomputable def stdSimplex.pick {n : ℕ+} (x y : ↑(stdSimplex ℝ (Fin ↑n))) : ↑{i : Fin ↑n | ↑x i ≤ ↑y i}

Equations

• stdSimplex.pick x y = Classical.choice ⋯

noncomputable def Fcolor {n l : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (x : ↑(TT n l)) : Fin ↑n

Equations

• Fcolor f x = ↑(stdSimplex.pick (TTtostdSimplex x) (f (TTtostdSimplex x)))

noncomputable def room_seq {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (l' : ℕ) : ↥(IndexedLOrder.colorful (Fcolor f))

Equations

• room_seq f l' = Classical.choice ⋯

@[instance_reducible]

noncomputable instance roomSeqCoestdSimplex {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (l' : ℕ) : CoeOut ↥(↑(room_seq f l')).1 ↑(stdSimplex ℝ (Fin ↑n))

Equations

• roomSeqCoestdSimplex f l' = { coe := fun (x : ↥(↑(room_seq f l')).1) => TTtostdSimplex ↑x }

noncomputable def room_point_seq {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (l' : ℕ) : ↥(↑(room_seq f l')).1

Equations

• room_point_seq f l' = IndexedLOrder.pick_colorful_point ⋯

def mk_subseq (f : ℕ → ℕ) (h : ∀ (n : ℕ), n < f n) : ℕ → ℕ

Equations

• mk_subseq f h 0 = f 0
• mk_subseq f h n.succ = f (mk_subseq f h n)

theorem exists_subseq_constant_of_finite_image {α : Type u_1} {s : Finset α} (e : ℕ → α) (he : ∀ (n : ℕ), e n ∈ s) : ∃ a ∈ s, ∃ (g : ℕ ↪o ℕ), ∀ (n : ℕ), e (g n) = a

theorem constant_index_set_nonempty {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : Nonempty ↑{(a, g) : Finset (Fin ↑n) × (ℕ ↪o ℕ) | ∀ (l' : ℕ), (↑(room_seq f (g l'))).2 = a}

noncomputable def gpkg {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : ↑{(a, g) : Finset (Fin ↑n) × (ℕ ↪o ℕ) | ∀ (l' : ℕ), (↑(room_seq f (g l'))).2 = a}

Equations

• gpkg f = Classical.choice ⋯

@[reducible, inline]

noncomputable abbrev g1 {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : ℕ ↪o ℕ

Equations

• g1 f = (↑(gpkg f)).2

theorem dominant_coords_tend_to_zero {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (C : Finset (Fin ↑n)) (g : ℕ ↪o ℕ) (h_const : ∀ (l' : ℕ), (↑(room_seq f (g l'))).2 = C) (i : Fin ↑n) : i ∉ C → Filter.Tendsto (fun (l' : ℕ) => ↑(TTtostdSimplex ↑(room_point_seq f (g l'))) i) Filter.atTop (nhds 0)

theorem hpkg_aux {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : Nonempty ↑{(z, h) : ↑(stdSimplex ℝ (Fin ↑n)) × (ℕ → ℕ) | StrictMono h ∧ Filter.Tendsto ((fun (l' : ℕ) => TTtostdSimplex ↑(room_point_seq f ((g1 f) l'))) ∘ h) Filter.atTop (nhds z)}

noncomputable def hpkg {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : ↑{(z, h) : ↑(stdSimplex ℝ (Fin ↑n)) × (ℕ → ℕ) | StrictMono h ∧ Filter.Tendsto ((fun (l' : ℕ) => TTtostdSimplex ↑(room_point_seq f ((g1 f) l'))) ∘ h) Filter.atTop (nhds z)}

Equations

• hpkg f = Classical.choice ⋯

theorem tendsto_diam_to_zero {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : Filter.Tendsto (fun (k : ℕ) => Metric.diam ↑(Finset.image (fun (x : ↑(TT n ⟨(g1 f) ((↑(hpkg f)).2 k) + 1, ⋯⟩)) => TTtostdSimplex x) (↑(room_seq f ((g1 f) ((↑(hpkg f)).2 k)))).1)) Filter.atTop (nhds 0)

theorem f_coords_ge_z_coords {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (hf : Continuous f) (i : Fin ↑n) : i ∈ (↑(gpkg f)).1 → ↑(f (↑(hpkg f)).1) i ≥ ↑(↑(hpkg f)).1 i

theorem Brouwer {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (hf : Continuous f) : ∃ (x : ↑(stdSimplex ℝ (Fin ↑n))), f x = x