Theorem: ProbabilityTheory.iIndep_comap_iff (LeanCamCombi/Mathlib/Probability/Independence/Basic.lean)

State before:
Ω : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝ : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
S : Finset ι
s : ι → Set Ω
f : (i : ι) → Ω → β i
⊢ iIndep (fun i => MeasurableSpace.comap (fun x => x ∈ s i) ⊤) μ ↔ iIndepSet s μ
Tactic:
simp_rw [← generateFrom_singleton]
State after:
Ω : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝ : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
S : Finset ι
s : ι → Set Ω
f : (i : ι) → Ω → β i
⊢ iIndep (fun i => generateFrom {s i}) μ ↔ iIndepSet s μ

State before:
Ω : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝ : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
S : Finset ι
s : ι → Set Ω
f : (i : ι) → Ω → β i
⊢ iIndep (fun i => generateFrom {s i}) μ ↔ iIndepSet s μ
Tactic:
rfl
State after:
no goals