shortestPrefixDiff_pos — Mathlib

English

If s is closed and nonempty and x ∉ s then 0 < shortestPrefixDiff x s.

Русский

Если s замкнуто и непусто и x ∉ s, то 0 < shortestPrefixDiff(x,s).

LaTeX

$$$$ 0 < shortestPrefixDiff(x,s) $$$$

Lean4

theorem shortestPrefixDiff_pos {s : Set (∀ n, E n)} (hs : IsClosed s) (hne : s.Nonempty) {x : ∀ n, E n} (hx : x ∉ s) :
    0 < shortestPrefixDiff x s := by
  rcases hne with ⟨y, hy⟩
  exact (zero_le _).trans_lt (firstDiff_lt_shortestPrefixDiff hs hx hy)

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