English
If there exists j ∈ Icc(n,m) with u j ω ∈ s, then the value stoppedValue u (hitting u s n m) ω lies in s.
Русский
Если существует j ∈ Icc(n,m) such that u j ω ∈ s, тогда остановленное значение stoppedValue u (hitting u s n m) ω принадлежит s.
LaTeX
$$$\\forall \\omega,\\ (\\exists j\\in \\mathrm{Icc}(n,m),\\ u(j,\\omega)\\in s) \\Rightarrow\\ stoppedValue\\ u\\ (hitting\\ u\\ s\\ n\\ m)\\omega \\in s.$$$
Lean4
theorem stoppedValue_hitting_mem [ConditionallyCompleteLinearOrder ι] [WellFoundedLT ι] {u : ι → Ω → β} {s : Set β}
{n m : ι} {ω : Ω} (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) : stoppedValue u (hitting u s n m) ω ∈ s :=
by
simp only [stoppedValue, hitting, if_pos h]
obtain ⟨j, hj₁, hj₂⟩ := h
have : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s} :=
csInf_mem (Set.nonempty_of_mem ⟨hj₁, hj₂⟩)
exact this.2
