le_hitting_of_exists — Mathlib

English

If a lower index is less than or equal to the hitting time, then certain inequalities hold comparing hitting to that index; in particular, hitting is bounded by the index.

Русский

Если левая граница не превосходит время попадания, то выполняются неравенства между hitting и этой границей; в частности hitting не превосходит индекс.

LaTeX

$$$n\leq i \Rightarrow (\text{hitting}(u,s,n,m,\omega) \le i)$ under appropriate assumptions.$$

Lean4

theorem le_hitting_of_exists {m : ι} (h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s) : n ≤ hitting u s n m ω :=
  by
  refine le_hitting ?_ ω
  by_contra h
  rw [Set.Icc_eq_empty_of_lt (not_le.mp h)] at h_exists
  simp at h_exists

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