disjoint_cylinder_of_longestPrefix_lt

English

If longestPrefix x s < n then s is disjoint from cylinder(x,n).

Русский

Если longestPrefix(x,s) < n, то s не пересекается с cylinder(x,n).

LaTeX

$$$$ \operatorname{longestPrefix}(x,s) < n \Rightarrow s \cap \mathrm{cylinder}(x,n) = \varnothing $$$$

Lean4

theorem disjoint_cylinder_of_longestPrefix_lt {s : Set (∀ n, E n)} (hs : IsClosed s) {x : ∀ n, E n} (hx : x ∉ s) {n : ℕ}
    (hn : longestPrefix x s < n) : Disjoint s (cylinder x n) :=
  by
  contrapose! hn
  rcases not_disjoint_iff_nonempty_inter.1 hn with ⟨y, ys, hy⟩
  apply le_trans _ (firstDiff_le_longestPrefix hs hx ys)
  apply (mem_cylinder_iff_le_firstDiff (ne_of_mem_of_not_mem ys hx).symm _).1
  rwa [mem_cylinder_comm]

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