English
An element s₂ belongs to ε-closure of {s₁} iff there exists n with a path of length n from s₁ to s₂ consisting of None steps.
Русский
s₂ ∈ εClosure({s₁}) ⇔ ∃n, IsPath s₁ s₂ (replicate n none).
LaTeX
$$$s_2 \in M.\\varepsilonClosure \{ s_1 \} \\Leftrightarrow \exists n, M.IsPath s_1 s_2 (\\mathrm{replicate}\ n \ \mathrm{none})$$$
Lean4
theorem mem_εClosure_iff_exists_path {s₁ s₂ : σ} : s₂ ∈ M.εClosure { s₁ } ↔ ∃ n, M.IsPath s₁ s₂ (.replicate n none)
where
mp
h := by
induction h with
| base t =>
use 0
subst t
apply IsPath.nil
| step _ _ _ _ ih =>
obtain ⟨n, _⟩ := ih
use n + 1
rw [List.replicate_add, isPath_append]
tauto
mpr := by
intro ⟨n, h⟩
induction n generalizing s₂
· rw [List.replicate_zero] at h
apply IsPath.eq_of_nil at h
solve_by_elim
· simp_rw [List.replicate_add, isPath_append, List.replicate_one, isPath_singleton] at h
obtain ⟨t, _, _⟩ := h
solve_by_elim [εClosure.step]
