FiniteIntervalPartition.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Turning convex finite fibers into exact integer interval pieces

theorem OAI.Ostmann.finite_convex_set_interval line 15
Source documentation
A finite set of consecutive natural numbers is an interval whose length is exactly its cardinality, including the empty case.
```
theorem finite_convex_set_interval (s : Finset ℕ)
    (hc : ∀ x ∈ s, ∀ y ∈ s, ∀ z, x ≤ z → z ≤ y → z ∈ s) :
    ∃ a : ℕ, s = Finset.Ico a (a + s.card) := by
…
```

theorem OAI.Ostmann.exists_finite_interval_partition line 41

Source documentation

The fibers of a code on an integer interval become consecutive subintervals. This provides the exact bijection needed by the character-sum partition.

theorem exists_finite_interval_partition {I : Type*} (N : ℕ) (code : ℕ → I)
    (hc : ∀ x y z, x < N → y < N → x ≤ z → z ≤ y →
      code x = code y → code z = code x) :
    ∃ (a K : I → ℕ) (e : Fin N ≃ Σ i, Fin (K i)),
      (∀ i (j : Fin (K i)), (e.symm ⟨i, j⟩).val = a i + j.val) ∧
      (∀ i (j : Fin (K i)), code (a i + j.val) = i) := by
…