firstDiff_lt_shortestPrefixDiff — Mathlib

English

firstDiff is the smallest index where two functions differ; it relates to longestPrefix via inequalities.

Русский

firstDiff — наименьший индекс, на котором две функции различаются; он связан с longestPrefix неравенствами.

LaTeX

$$$$ \text{firstDiff}(x,y) \le \text{longestPrefix}(x,s) $$$$

Lean4

theorem firstDiff_lt_shortestPrefixDiff {s : Set (∀ n, E n)} (hs : IsClosed s) {x y : ∀ n, E n} (hx : x ∉ s)
    (hy : y ∈ s) : firstDiff x y < shortestPrefixDiff x s :=
  by
  have A := exists_disjoint_cylinder hs hx
  rw [shortestPrefixDiff, dif_pos A]
  classical
  have B := Nat.find_spec A
  contrapose! B
  rw [not_disjoint_iff_nonempty_inter]
  refine ⟨y, hy, ?_⟩
  rw [mem_cylinder_comm]
  exact cylinder_anti y B (mem_cylinder_firstDiff x y)

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