hitting_eq_sInf — Mathlib

English

For any ω, the hitting time from bottom to top equals the infimum of indices i with u i ω ∈ s: hitting u s ⊥ ⊤ ω = sInf { i ∈ ι | u i ω ∈ s }.

Русский

Для каждого ω попадание от нижнего до верхнего предела равно наименьшей верхней границе: hitting u s ⊥ ⊤ ω = sInf { i ∈ ι | u i ω ∈ s }.

LaTeX

$$$\\forall \\omega,\\ hitting\\ u\\ s\\ \\perp\\ \\top\\ \\omega = \\inf\\{i\\in ι\\;|\;u(i,\\omega)∈ s\\}.$$$

Lean4

theorem hitting_eq_sInf (ω : Ω) : hitting u s ⊥ ⊤ ω = sInf {i : ι | u i ω ∈ s} :=
  by
  simp only [hitting, Set.Icc_bot, Set.Iic_top, Set.univ_inter, ite_eq_left_iff, not_exists]
  intro h_notMem_s
  symm
  rw [sInf_eq_top]
  simp only [Set.mem_univ, true_and] at h_notMem_s
  exact fun i hi_mem_s => absurd hi_mem_s (h_notMem_s i)

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