Supporting results for pointwise provable equality.

def PointwiseComposition.Nat.cases {α : ℕ → Sort u} (hzero : α 0) (hsucc : (n : ℕ) → α (n + 1)) (n : ℕ) : α n

The cases construction in Nat.

Equations

• (hzero :>ₙ hsucc) 0 = hzero
• (hzero :>ₙ hsucc) n.succ = hsucc n

def PointwiseComposition.Nat.«term_:>ₙ_» : Lean.TrailingParserDescr

The «term :>ₙ » construction in Nat.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.Nat.cases_zero {α : ℕ → Sort u} (hzero : α 0) (hsucc : (n : ℕ) → α (n + 1)) : (hzero :>ₙ hsucc) 0 = hzero

@[simp]

theorem PointwiseComposition.Nat.cases_succ {α : ℕ → Sort u} (hzero : α 0) (hsucc : (n : ℕ) → α (n + 1)) (n : ℕ) : (hzero :>ₙ hsucc) (n + 1) = hsucc n

@[simp]

theorem PointwiseComposition.Nat.ne_step_max (n m : ℕ) : n ≠ max n m + 1

@[simp]

theorem PointwiseComposition.Nat.ne_step_max' (n m : ℕ) : n ≠ max m n + 1

theorem PointwiseComposition.Nat.rec_eq {α : Sort u_1} (a : α) (f₁ f₂ : ℕ → α → α) (n : ℕ) (H : ∀ m < n, ∀ (a : α), f₁ m a = f₂ m a) : Nat.rec a f₁ n = Nat.rec a f₂ n

theorem PointwiseComposition.Nat.least_number (P : ℕ → Prop) (hP : ∃ (x : ℕ), P x) : ∃ (x : ℕ), P x ∧ ∀ z < x, ¬P z

def PointwiseComposition.Nat.toFin (n a✝ : ℕ) : Option (Fin n)

The to Fin construction in Nat.

Equations

• PointwiseComposition.Nat.toFin n x = if hx : x < n then some ⟨x, hx⟩ else none

theorem PointwiseComposition.Nat.zero_lt_of_not_zero {n : ℕ} (hn : n ≠ 0) : 0 < n

theorem PointwiseComposition.Nat.one_le_of_bodd {n : ℕ} (h : n.bodd = true) : 1 ≤ n

theorem PointwiseComposition.Nat.pair_le_pair_of_le {a₁ a₂ b₁ b₂ : ℕ} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : Nat.pair a₁ b₁ ≤ Nat.pair a₂ b₂