hitting_le_iff_of_lt — Mathlib

English

If i < m, then hitting u s n m ω ≤ i is equivalent to the existence of j ∈ [n,i] with u_j ω ∈ s.

Русский

Если i < m, то hitting ≤ i эквивалентно существованию j ∈ [n,i] с u_j(ω) ∈ s.

LaTeX

$$$\text{hitting}(u,s,n,m,\omega) ≤ i \iff \exists j\in [n,i], u_j(\omega)\in s$$$

Lean4

theorem hitting_le_iff_of_lt [WellFoundedLT ι] {m : ι} (i : ι) (hi : i < m) :
    hitting u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s :=
  by
  by_cases h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
  · rw [hitting_le_iff_of_exists h_exists]
  · simp_rw [hitting, if_neg h_exists]
    push_neg at h_exists
    simp only [not_le.mpr hi, Set.mem_Icc, false_iff, not_exists, not_and, and_imp]
    exact fun k hkn hki => h_exists k ⟨hkn, hki.trans hi.le⟩

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