Indexing types

This file introduces IndexType : ℕ → Type such that IndexType 0 = ℕ and IndexType (N+1) = Fin (N+1). Each IndexType N has a total order and and inductive principle together with supporting lemmas.

def IndexType (n : ℕ) : Type

Our model indexing type depending on n : ℕ is ℕ if n = 0 and Fin n otherwise

Equations

• IndexType n = Nat.casesOn n ℕ fun (k : ℕ) => Fin (k + 1)

def IndexType.fromNat {N : ℕ} : ℕ → IndexType N

Equations

• IndexType.fromNat = id
• IndexType.fromNat = Nat.cast

def IndexType.toNat {N : ℕ} : IndexType N → ℕ

Equations

• IndexType.toNat = id
• IndexType.toNat = Fin.val

@[simp]

theorem indexType_zero : IndexType 0 = ℕ

@[simp]

theorem indexType_succ (n : ℕ) : IndexType (n + 1) = Fin (n + 1)

@[simp]

theorem indexType_of_zero_lt {n : ℕ} (h : 0 < n) : IndexType n = Fin n

instance instOrderBotIndexType (n : ℕ) : OrderBot (IndexType n)

Equations

• instOrderBotIndexType 0 = inferInstanceAs (OrderBot ℕ)
• instOrderBotIndexType N.succ = inferInstanceAs (OrderBot (Fin (N + 1)))

instance instLinearOrderIndexType (n : ℕ) : LinearOrder (IndexType n)

Equations

• instLinearOrderIndexType 0 = inferInstanceAs (LinearOrder ℕ)
• instLinearOrderIndexType N.succ = inferInstanceAs (LinearOrder (Fin (N + 1)))

instance instLocallyFiniteOrderIndexType (n : ℕ) : LocallyFiniteOrder (IndexType n)

Equations

• instLocallyFiniteOrderIndexType 0 = inferInstanceAs (LocallyFiniteOrder ℕ)
• instLocallyFiniteOrderIndexType N.succ = inferInstanceAs (LocallyFiniteOrder (Fin (N + 1)))

instance instZeroIndexType (n : ℕ) : Zero (IndexType n)

Equations

• instZeroIndexType 0 = inferInstanceAs (Zero ℕ)
• instZeroIndexType N.succ = inferInstanceAs (Zero (Fin (N + 1)))

instance instSuccOrderIndexType (n : ℕ) : SuccOrder (IndexType n)

Equations

• instSuccOrderIndexType 0 = inferInstanceAs (SuccOrder ℕ)
• instSuccOrderIndexType N.succ = inferInstanceAs (SuccOrder (Fin (N + 1)))

theorem Set.countable_iff_exists_nonempty_indexType_equiv {α : Type u_1} {s : Set α} (hne : s.Nonempty) : s.Countable ↔ ∃ (n : ℕ), Nonempty (IndexType n ≃ ↑s)

theorem IndexType.not_lt_zero {n : ℕ} (j : IndexType n) : ¬j < 0

theorem IndexType.zero_le {n : ℕ} (i : IndexType n) : 0 ≤ i

def IndexType.succ {N : ℕ} : IndexType N → IndexType N

Equations

• IndexType.succ = Order.succ

theorem IndexType.succ_castSuccEmb {n : ℕ} (i : Fin n) : succ i.castSucc = i.succ

theorem IndexType.succ_eq {n : ℕ} (i : IndexType n) : i.succ = i ↔ IsMax i

theorem IndexType.lt_succ {n : ℕ} (i : IndexType n) (h : ¬IsMax i) : i < i.succ

theorem IndexType.le_max {n : ℕ} {i : IndexType n} (h : IsMax i) (j : IndexType n) : j ≤ i

theorem IndexType.le_of_lt_succ {n : ℕ} (i : IndexType n) {j : IndexType n} (h : i < j.succ) : i ≤ j

theorem IndexType.exists_castSucc_eq {n : ℕ} (i : IndexType (n + 1)) (hi : ¬IsMax i) : ∃ (i' : Fin n), i'.castSucc = i

theorem IndexType.toNat_succ {n : ℕ} (i : IndexType n) (hi : ¬IsMax i) : i.succ.toNat = i.toNat + 1

theorem IndexType.not_isMax (n : IndexType 0) : ¬IsMax n

theorem IndexType.induction_from {n : ℕ} {P : IndexType n → Prop} {i₀ : IndexType n} (h₀ : P i₀) (ih : ∀ i ≥ i₀, ¬IsMax i → P i → P i.succ) (i : IndexType n) : i ≥ i₀ → P i

theorem IndexType.induction {n : ℕ} {P : IndexType n → Prop} (h₀ : P 0) (ih : ∀ (i : IndexType n), ¬IsMax i → P i → P i.succ) (i : IndexType n) : P i

theorem IndexType.exists_by_induction {n : ℕ} {α : Type u_1} (P : IndexType n → α → Prop) (Q : IndexType n → α → α → Prop) (h₀ : ∃ (a : α), P 0 a) (ih : ∀ (n_1 : IndexType n) (a : α), P n_1 a → ¬IsMax n_1 → ∃ (a' : α), P n_1.succ a' ∧ Q n_1 a a') : ∃ (f : IndexType n → α), ∀ (n_1 : IndexType n), P n_1 (f n_1) ∧ (¬IsMax n_1 → Q n_1 (f n_1) (f n_1.succ))