firstDiff_le_longestPrefix — Mathlib

English

If s is closed and x,y ∉ s, then firstDiff(x,y) ≤ longestPrefix(x,s).

Русский

Если s замкнуто и x,y ∉ s, то firstDiff(x,y) ≤ longestPrefix(x,s).

LaTeX

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

Lean4

theorem firstDiff_le_longestPrefix {s : Set (∀ n, E n)} (hs : IsClosed s) {x y : ∀ n, E n} (hx : x ∉ s) (hy : y ∈ s) :
    firstDiff x y ≤ longestPrefix x s := by
  rw [longestPrefix, le_tsub_iff_right]
  · exact firstDiff_lt_shortestPrefixDiff hs hx hy
  · exact shortestPrefixDiff_pos hs ⟨y, hy⟩ hx

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