English
For a closed nonempty s and any x, the intersection s ∩ cylinder(x, longestPrefix x s) is nonempty.
Русский
Для замкнутого непустого s и любого x пересечение s ∩ cylinder(x, longestPrefix x s) непусто.
LaTeX
$$$$ (s \cap \mathrm{cylinder}(x, \text{longestPrefix}(x,s))).\text{Nonempty} $$$$
Lean4
theorem inter_cylinder_longestPrefix_nonempty {s : Set (∀ n, E n)} (hs : IsClosed s) (hne : s.Nonempty) (x : ∀ n, E n) :
(s ∩ cylinder x (longestPrefix x s)).Nonempty :=
by
by_cases hx : x ∈ s
· exact ⟨x, hx, self_mem_cylinder _ _⟩
have A := exists_disjoint_cylinder hs hx
have B : longestPrefix x s < shortestPrefixDiff x s := Nat.pred_lt (shortestPrefixDiff_pos hs hne hx).ne'
rw [longestPrefix, shortestPrefixDiff, dif_pos A] at B ⊢
classical
obtain ⟨y, ys, hy⟩ : ∃ y : ∀ n : ℕ, E n, y ∈ s ∧ x ∈ cylinder y (Nat.find A - 1) := by
simpa only [not_disjoint_iff, mem_cylinder_comm] using Nat.find_min A B
refine ⟨y, ys, ?_⟩
rw [mem_cylinder_iff_eq] at hy ⊢
rw [hy]
