min_firstDiff_le — Mathlib

English

Let x,y,z be sequences. If x ≠ z, then min(firstDiff x y, firstDiff y z) ≤ firstDiff x z.

Русский

Пусть x,y,z — последовательности. Если x ≠ z, то min(firstDiff x y, firstDiff y z) ≤ firstDiff x z.

LaTeX

$$$\\forall x,y,z:\\, (x \\neq z) \\Rightarrow \\min\\big(\\operatorname{firstDiff}(x,y),\\operatorname{firstDiff}(y,z)\\big) \\le \\operatorname{firstDiff}(x,z)$$$

Lean4

theorem min_firstDiff_le (x y z : ∀ n, E n) (h : x ≠ z) : min (firstDiff x y) (firstDiff y z) ≤ firstDiff x z :=
  by
  by_contra! H
  rw [lt_min_iff] at H
  refine apply_firstDiff_ne h ?_
  calc
    x (firstDiff x z) = y (firstDiff x z) := apply_eq_of_lt_firstDiff H.1
    _ = z (firstDiff x z) := apply_eq_of_lt_firstDiff H.2

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