firstDiff_comm — Mathlib

English

For any two sequences x,y, the first index where they differ is symmetric: firstDiff x y = firstDiff y x.

Русский

Для любых последовательностей x, y первый индекс, на котором они различаются, симметричен: firstDiff x y = firstDiff y x.

LaTeX

$$$\\operatorname{firstDiff}(x,y)=\\operatorname{firstDiff}(y,x)$$$

Lean4

theorem firstDiff_comm (x y : ∀ n, E n) : firstDiff x y = firstDiff y x := by
  classical simp only [firstDiff_def, ne_comm]

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