apply_firstDiff_ne — Mathlib

English

If x ≠ y, then the values at the first differing index are different: x(firstDiff x y) ≠ y(firstDiff x y).

Русский

Если x ≠ y, то значения в первой точке различия различны: x(firstDiff x y) ≠ y(firstDiff x y).

LaTeX

$$$x(\\\\text{firstDiff}(x,y)) \\\\neq y(\\\\text{firstDiff}(x,y))$$$

Lean4

theorem apply_firstDiff_ne {x y : ∀ n, E n} (h : x ≠ y) : x (firstDiff x y) ≠ y (firstDiff x y) :=
  by
  rw [firstDiff_def, dif_pos h]
  classical exact Nat.find_spec (ne_iff.1 h)

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