hitting_le_of_mem — Mathlib

English

If there exists a hit in [n,m], then hitting u s n m ω ≤ i is equivalent to the existence of a hit in [n,i].

Русский

Если существует попадание в интервале [n,m], то hitting ≤ i эквивалентно существованию попадания в [n,i].

LaTeX

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

Lean4

theorem hitting_le_of_mem {m : ι} (hin : n ≤ i) (him : i ≤ m) (his : u i ω ∈ s) : hitting u s n m ω ≤ i :=
  by
  have h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s := ⟨i, ⟨hin, him⟩, his⟩
  simp_rw [hitting, if_pos h_exists]
  exact csInf_le (BddBelow.inter_of_left bddBelow_Icc) (Set.mem_inter ⟨hin, him⟩ his)

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