apply_eq_of_lt_firstDiff — Mathlib

English

Let x and y be sequences x: ∀ n, E n and y: ∀ n, E n. If n is strictly less than the first index where x and y differ, then x n = y n.

Русский

Пусть x и y — последовательности x: ∀ n, E n и y: ∀ n, E n. Если n меньше первого индекса, в котором x и y различаются, то x n = y n.

LaTeX

$$$\\forall x,y:\\,\\forall n:\\mathbb{N},\\ n < \\operatorname{firstDiff}(x,y) \\Rightarrow x(n)=y(n)$$$

Lean4

theorem apply_eq_of_lt_firstDiff {x y : ∀ n, E n} {n : ℕ} (hn : n < firstDiff x y) : x n = y n :=
  by
  rw [firstDiff_def] at hn
  split_ifs at hn with h
  · convert Nat.find_min (ne_iff.1 h) hn
    simp
  · exact (not_lt_zero' hn).elim

Похожие утверждения