E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x y : (n : ℕ) → E n
hx : ¬x ∈ s
hy : y ∈ s
⊢ firstDiff x y + 1 ≤ shortestPrefixDiff x s

E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x y : (n : ℕ) → E n
hx : ¬x ∈ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff x s
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
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
rw [longestPrefix, le_tsub_iff_right]
no goals
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x y : (n : ℕ) → E n
hx : ¬x ∈ s
hy : y ∈ s
⊢ firstDiff x y + 1 ≤ shortestPrefixDiff x s
exact firstDiff_lt_shortestPrefixDiff hs hx hy
no goals
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x y : (n : ℕ) → E n
hx : ¬x ∈ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff x s
exact shortestPrefixDiff_pos hs ⟨y, hy⟩ hx