measurableSet_eq — Mathlib

English

For any i, the set {ω ∈ Ω : τ(ω) = i} is measurable in F_i, since it equals {τ ≤ i} ∩ {τ ≥ i}.

Русский

Для любого i множество {ω ∈ Ω : τ(ω) = i} измеримо в F_i, так как это пересечение {τ ≤ i} и {τ ≥ i}.

LaTeX

$$$\forall i, \{\omega \in \Omega \mid \tau(\omega) = i\} \in \mathcal{F}_i \;\text{(since } \{\tau = i\} = \{\tau \le i\} \cap \{\tau \ge i\} \)$$$

Lean4

theorem measurableSet_eq (hτ : IsStoppingTime f τ) (i : ι) : MeasurableSet[f i] {ω | τ ω = i} :=
  by
  have : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i} := by ext1 ω;
    simp only [Set.mem_setOf_eq, Set.mem_inter_iff, le_antisymm_iff]
  rw [this]
  exact (hτ.measurableSet_le i).inter (hτ.measurableSet_ge i)

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