English
Independence of two events s and t is equivalent to μ(t1 ∩ t2) = μ(t1) μ(t2) for all t1, t2 with t1 measurable w.r.t. generateFrom {s} and t2 measurable w.r.t. generateFrom {t}.
Русский
Независимость двух событий s и t эквивалентна равенству μ(t1 ∩ t2) = μ(t1) μ(t2) для любых t1, t2 измеримых относительно σ({s}) и σ({t}) соответственно.
LaTeX
$$$\text{IndepSet}(s,t,\mu) \iff \forall t_1,t_2,\; t_1 \text{ Measurable}[\ generateFrom\{s\}] (t_1) \to t_2 \text{ Measurable}[\ generateFrom\{t\}] (t_2) \to μ(t_1 \cap t_2) = μ(t_1) μ(t_2)$$$
Lean4
theorem IndepSet_iff (s t : Set Ω) (μ : Measure Ω) :
IndepSet s t μ ↔
∀ t1 t2,
MeasurableSet[generateFrom { s }] t1 → MeasurableSet[generateFrom { t }] t2 → μ (t1 ∩ t2) = μ t1 * μ t2 :=
by simp only [IndepSet_iff_Indep, Indep_iff]
