hitting_eq_end_iff — Mathlib

English

The hitting time equals m if there is no hitting j in [n,m]; equivalently, if there exists a first time in [n,m] where u_j ∈ s, then the equality with m fails and the Inf-operator produces a smaller value.

Русский

Если попадания в [n,m] нет, hitting = m; иначе hitting < m и Inf даёт меньшее значение.

LaTeX

$$$\text{hitting}(u,s,n,m) = m \iff \text{no } j\in [n,m]\text{ with } u_j\in s$$$

Lean4

theorem hitting_eq_end_iff {m : ι} :
    hitting u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m := by
  classical rw [hitting, ite_eq_right_iff]

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