English
A collection of standard lemmas governs hitting times: monotonicity in the upper bound, relationship with exists-hit, and equivalence of lt/≤ statements via hits.
Русский
Набор стандартных лемм про время попадания: монотонность верхней границы, связь с существованием попадания, эквивалентности между отношениями < и ≤ через попадание.
LaTeX
$$$\text{(standard hitting lemmas)}$$$
Lean4
theorem hitting_of_le {m : ι} (hmn : m ≤ n) : hitting u s n m ω = m :=
by
obtain rfl | h := le_iff_eq_or_lt.1 hmn
·
classical
rw [hitting, ite_eq_right_iff, forall_exists_index]
conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
intro i hi₁ hi₂ hi
rw [Set.inter_eq_left.2, csInf_singleton]
exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)
· exact hitting_of_lt h
