hitting_bot_le_iff — Mathlib

English

If there exists j ≤ n with u j ω ∈ s, then for all i, hitting u s ⊥ n ω ≤ i is equivalent to ∃ j ≤ i with u j ω ∈ s.

Русский

Если существует j ≤ n с u j ω ∈ s, то для всех i верно: hitting u s ⊥ n ω ≤ i тогда и только если ∃ j ≤ i с u j ω ∈ s.

LaTeX

$$$\\exists j\\le n,\\ u j\\omega ∈ s\\Rightarrow\\ hitting\\ u\\ s\\ bot\\ n\\ ω\\le i\\;\\Leftrightarrow\\; \\exists j\\le i,\\ u j\\omega ∈ s.$$$

Lean4

theorem hitting_bot_le_iff {i n : ι} {ω : Ω} (hx : ∃ j, j ≤ n ∧ u j ω ∈ s) :
    hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s :=
  by
  rcases lt_or_ge i n with hi | hi
  · rw [hitting_le_iff_of_lt _ hi]
    simp
  · simp only [(hitting_le ω).trans hi, true_iff]
    obtain ⟨j, hj₁, hj₂⟩ := hx
    exact ⟨j, hj₁.trans hi, hj₂⟩

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