ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>f g : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.codeSupp (f.case g) k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.case g) k) ∪ (Turing.PartrecToTM2.codeSupp f k ∪ Turing.PartrecToTM2.codeSupp g k)
<VAR>f : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.codeSupp f.fix k = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal f.fix k) ∪ Turing.PartrecToTM2.codeSupp f (Turing.PartrecToTM2.Cont'.fix f k)
<VAR>fs : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.cons₁ fs k) = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux (Turing.PartrecToTM2.move₂ (fun s => decide (s = Turing.PartrecToTM2.Γ'.consₗ)) Turing.PartrecToTM2.K'.stack Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.trNormal fs k.cons₂)))) ∪ Turing.PartrecToTM2.codeSupp fs k.cons₂
<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.contSupp k.cons₂ = Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)) ∪ Turing.PartrecToTM2.contSupp k
<VAR>f : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.comp f k) = Turing.PartrecToTM2.codeSupp f k
<VAR>f : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.fix f k) = Turing.PartrecToTM2.codeSupp f (Turing.PartrecToTM2.Cont'.fix f k)
<GOAL>Turing.PartrecToTM2.contSupp Turing.PartrecToTM2.Cont'.halt = ∅
<VAR>K S : Finset Turing.PartrecToTM2.Λ'<VAR>q : Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.Supports (insert q K) S ↔ Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr q) ∧ Turing.PartrecToTM2.Supports K S
<VAR>S : Finset Turing.PartrecToTM2.Λ'<VAR>q : Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.Supports {q} S ↔ Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr q)
<VAR>K₁ K₂ S : Finset Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.Supports (K₁ ∪ K₂) S ↔ Turing.PartrecToTM2.Supports K₁ S ∧ Turing.PartrecToTM2.Supports K₂ S
<VAR>K : Option Turing.PartrecToTM2.Γ' → Finset Turing.PartrecToTM2.Λ'<VAR>S : Finset Turing.PartrecToTM2.Λ'<GOAL>Turing.PartrecToTM2.Supports (Finset.univ.biUnion K) S ↔ ∀ (a : Option Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.Supports (K a) S
<VAR>S : Finset Turing.PartrecToTM2.Λ'<VAR>k : Turing.PartrecToTM2.K'<VAR>q : Turing.PartrecToTM2.Λ'<VAR>H : Turing.PartrecToTM2.Λ'.Supports S q<GOAL>Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.head k q)
<VAR>S : Finset Turing.PartrecToTM2.Λ'<VAR>k : Turing.PartrecToTM2.Cont'<VAR>H₁ : Turing.PartrecToTM2.contSupp k ⊆ S<GOAL>Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret k))
<VAR>S : Finset Turing.PartrecToTM2.Λ'<VAR>q : Turing.PartrecToTM2.Λ'<VAR>H₁ : Turing.PartrecToTM2.Λ'.Supports S q<VAR>HS₁ : Turing.PartrecToTM2.trStmts₁ q ⊆ S<GOAL>Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.trStmts₁ q) S
<VAR>S : Finset Turing.PartrecToTM2.Λ'<VAR>q : Turing.PartrecToTM2.Λ'<VAR>K : Finset Turing.PartrecToTM2.Λ'<VAR>H₁ : Turing.PartrecToTM2.Λ'.Supports S q<VAR>H₂ : Turing.PartrecToTM2.trStmts₁ q ∪ K ⊆ S<VAR>H₃ : K ⊆ S → Turing.PartrecToTM2.Supports K S<GOAL>Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.trStmts₁ q ∪ K) S
<VAR>S : Finset Turing.PartrecToTM2.Λ'<VAR>c : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<VAR>Hk : Turing.PartrecToTM2.codeSupp c k ⊆ S<GOAL>Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.trNormal c k)
<VAR>S : Finset Turing.PartrecToTM2.Λ'<VAR>c : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<VAR>H : Turing.PartrecToTM2.codeSupp c k ⊆ S<GOAL>Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.codeSupp' c k) S
<VAR>S : Finset Turing.PartrecToTM2.Λ'<VAR>k : Turing.PartrecToTM2.Cont'<VAR>H : Turing.PartrecToTM2.contSupp k ⊆ S<GOAL>Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.contSupp k) S
<VAR>S : Finset Turing.PartrecToTM2.Λ'<VAR>c : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<VAR>H : Turing.PartrecToTM2.codeSupp c k ⊆ S<GOAL>Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.codeSupp c k) S
<VAR>c : Turing.ToPartrec.Code<VAR>k : Turing.PartrecToTM2.Cont'<GOAL>Turing.TM2.Supports Turing.PartrecToTM2.tr (Turing.PartrecToTM2.codeSupp c k)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>π : ι → Set (Set Ω)<VAR>hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.iCondIndepSets m' hm' π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s1 s2 : Set (Set Ω)<VAR>hs1 : ∀ s ∈ s1, MeasurableSet s<VAR>hs2 : ∀ s ∈ s2, MeasurableSet s<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndepSets m' hm' s1 s2 μ ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᵐ[μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s : ι → Set Ω<VAR>hπ : ∀ (i : ι), MeasurableSet (s i)<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.iCondIndepSets m' hm' (fun i => {s i}) μ ↔ ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>ProbabilityTheory.CondIndepSets m' hm' {s} {t} μ ↔ μ[(s ∩ t).indicator fun ω => 1|m'] =ᵐ[μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>m : ι → MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.iCondIndep m' hm' m μ ↔ ProbabilityTheory.iCondIndepSets m' hm' (fun x => {s | MeasurableSet s}) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>m : ι → MeasurableSpace Ω<VAR>hm : ∀ (i : ι), m i ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.iCondIndep m' hm' m μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>m' m₁ m₂ : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ ↔ ProbabilityTheory.CondIndepSets m' hm' {s | MeasurableSet s} {s | MeasurableSet s} μ
<VAR>Ω : Type u_1<VAR>m' m₁ m₂ : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>hm₁ : m₁ ≤ mΩ<VAR>hm₂ : m₂ ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᵐ[μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s : ι → Set Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.iCondIndepSet m' hm' s μ ↔ ProbabilityTheory.iCondIndep m' hm' (fun i => MeasurableSpace.generateFrom {s i}) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s : ι → Set Ω<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.iCondIndepSet m' hm' s μ ↔ ProbabilityTheory.iCondIndepSets m' hm' (fun i => {s i}) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s : ι → Set Ω<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.iCondIndepSet m' hm' s μ ↔ ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s t : Set Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndepSet m' hm' s t μ ↔ ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s}) (MeasurableSpace.generateFrom {t}) hm' μ
<VAR>Ω : Type u_1<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s t : Set Ω<VAR>hs_meas : MeasurableSet s<VAR>ht_meas : MeasurableSet t<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndepSet m' hm' s t μ ↔ ProbabilityTheory.CondIndepSets m' hm' {s} {t} μ
<VAR>Ω : Type u_1<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndepSet m' hm' s t μ ↔ μ[(s ∩ t).indicator fun ω => 1|m'] =ᵐ[μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>β : ι → Type u_3<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (x : ι) → Ω → β x<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.iCondIndepFun m' hm' m f μ ↔ ProbabilityTheory.iCondIndep m' hm' (fun x => MeasurableSpace.comap (f x) (m x)) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>β : ι → Type u_3<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (x : ι) → Ω → β x<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.iCondIndepFun m' hm' m f μ ↔ ∀ (s : Finset ι) {g : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (g i)) → μ[(⋂ i ∈ s, g i).indicator fun ω => 1|m'] =ᵐ[μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : Ω → β<VAR>g : Ω → γ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndepFun m' hm' f g μ ↔ ProbabilityTheory.CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ
<VAR>Ω : Type u_1<VAR>m' : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : Ω → β<VAR>g : Ω → γ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndepFun m' hm' f g μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᵐ[μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s₁ s₂ : Set (Set Ω)<VAR>h : ProbabilityTheory.CondIndepSets m' hm' s₁ s₂ μ<GOAL>ProbabilityTheory.CondIndepSets m' hm' s₂ s₁ μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s₁ s₂ s₃ : Set (Set Ω)<VAR>h_indep : ProbabilityTheory.CondIndepSets m' hm' s₁ s₂ μ<VAR>h31 : s₃ ⊆ s₁<GOAL>ProbabilityTheory.CondIndepSets m' hm' s₃ s₂ μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s₁ s₂ s₃ : Set (Set Ω)<VAR>h_indep : ProbabilityTheory.CondIndepSets m' hm' s₁ s₂ μ<VAR>h32 : s₃ ⊆ s₂<GOAL>ProbabilityTheory.CondIndepSets m' hm' s₁ s₃ μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s₁ s₂ s' : Set (Set Ω)<VAR>h₁ : ProbabilityTheory.CondIndepSets m' hm' s₁ s' μ<VAR>h₂ : ProbabilityTheory.CondIndepSets m' hm' s₂ s' μ<GOAL>ProbabilityTheory.CondIndepSets m' hm' (s₁ ∪ s₂) s' μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s₁ s₂ s' : Set (Set Ω)<GOAL>ProbabilityTheory.CondIndepSets m' hm' (s₁ ∪ s₂) s' μ ↔ ProbabilityTheory.CondIndepSets m' hm' s₁ s' μ ∧ ProbabilityTheory.CondIndepSets m' hm' s₂ s' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>hyp : ∀ (n : ι), ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ<GOAL>ProbabilityTheory.CondIndepSets m' hm' (⋃ n, s n) s' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>u : Set ι<VAR>hyp : ∀ n ∈ u, ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ<GOAL>ProbabilityTheory.CondIndepSets m' hm' (⋃ n ∈ u, s n) s' μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s₁ s' : Set (Set Ω)<VAR>s₂ : Set (Set Ω)<VAR>h₁ : ProbabilityTheory.CondIndepSets m' hm' s₁ s' μ<GOAL>ProbabilityTheory.CondIndepSets m' hm' (s₁ ∩ s₂) s' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>h : ∃ n, ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ<GOAL>ProbabilityTheory.CondIndepSets m' hm' (⋂ n, s n) s' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>u : Set ι<VAR>h : ∃ n ∈ u, ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ<GOAL>ProbabilityTheory.CondIndepSets m' hm' (⋂ n ∈ u, s n) s' μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : Set Ω<GOAL>ProbabilityTheory.CondIndepSet m' hm' s ∅ μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : Set Ω<GOAL>ProbabilityTheory.CondIndepSet m' hm' ∅ s μ
<VAR>Ω : Type u_1<VAR>m' m₁ m₂ mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h : ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ<GOAL>ProbabilityTheory.CondIndep m' m₂ m₁ hm' μ
<VAR>Ω : Type u_1<VAR>m₁ : MeasurableSpace Ω<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndep m' m₁ ⊥ hm' μ
<VAR>Ω : Type u_1<VAR>m₁ : MeasurableSpace Ω<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndep m' ⊥ m₁ hm' μ
<VAR>Ω : Type u_1<VAR>m' m₁ m₂ m₃ mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_indep : ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ<VAR>h31 : m₃ ≤ m₁<GOAL>ProbabilityTheory.CondIndep m' m₃ m₂ hm' μ
<VAR>Ω : Type u_1<VAR>m' m₁ m₂ m₃ mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_indep : ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ<VAR>h32 : m₃ ≤ m₂<GOAL>ProbabilityTheory.CondIndep m' m₁ m₃ hm' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : ι → Set (Set Ω)<VAR>h_indep : ProbabilityTheory.iCondIndepSets m' hm' s μ<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>ProbabilityTheory.CondIndepSets m' hm' (s i) (s j) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>m : ι → MeasurableSpace Ω<VAR>h_indep : ProbabilityTheory.iCondIndep m' hm' m μ<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>ProbabilityTheory.CondIndep m' (m i) (m j) hm' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : ι → Type u_3<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (i : ι) → Ω → β i<VAR>hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' m f μ<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i) (f j) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>m : ι → MeasurableSpace Ω<VAR>s : ι → Set (Set Ω)<VAR>hms : ∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)<VAR>h_indep : ProbabilityTheory.iCondIndep m' hm' m μ<GOAL>ProbabilityTheory.iCondIndepSets m' hm' s μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s1 s2 : Set (Set Ω)<VAR>h_indep : ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) hm' μ<GOAL>ProbabilityTheory.CondIndepSets m' hm' s1 s2 μ
<VAR>Ω : Type u_1<VAR>m' m₁ m₂ mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>p1 p2 : Set (Set Ω)<VAR>h1 : m₁ ≤ mΩ<VAR>h2 : m₂ ≤ mΩ<VAR>hp1 : IsPiSystem p1<VAR>hp2 : IsPiSystem p2<VAR>hpm1 : m₁ = MeasurableSpace.generateFrom p1<VAR>hpm2 : m₂ = MeasurableSpace.generateFrom p2<VAR>hyp : ProbabilityTheory.CondIndepSets m' hm' p1 p2 μ<GOAL>ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>p1 p2 : Set (Set Ω)<VAR>hp1m : ∀ s ∈ p1, MeasurableSet s<VAR>hp2m : ∀ s ∈ p2, MeasurableSet s<VAR>hp1 : IsPiSystem p1<VAR>hp2 : IsPiSystem p2<VAR>hyp : ProbabilityTheory.CondIndepSets m' hm' p1 p2 μ<GOAL>ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom p1) (MeasurableSpace.generateFrom p2) hm' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : ι → Set (Set Ω)<VAR>S T : Set ι<VAR>h_indep : ProbabilityTheory.iCondIndepSets m' hm' s μ<VAR>hST : Disjoint S T<GOAL>ProbabilityTheory.CondIndepSets m' hm' (piiUnionInter s S) (piiUnionInter s T) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.iCondIndepSet m' hm' s μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {t | ∃ n ∈ S, s n = t}) (MeasurableSpace.generateFrom {t | ∃ k ∈ T, s k = t}) hm' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>m : ι → MeasurableSpace Ω<VAR>h_le : ∀ (i : ι), m i ≤ mΩ<VAR>h_indep : ProbabilityTheory.iCondIndep m' hm' m μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>ProbabilityTheory.CondIndep m' (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) hm' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' m₁ mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>m : ι → MeasurableSpace Ω<VAR>h_indep : ∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm' μ<VAR>h_le : ∀ (i : ι), m i ≤ mΩ<VAR>h_le' : m₁ ≤ mΩ<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<GOAL>ProbabilityTheory.CondIndep m' (⨆ i, m i) m₁ hm' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>Preorder ι<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.iCondIndepSet m' hm' s μ<VAR>i : ι<GOAL>ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s i}) (MeasurableSpace.generateFrom {t | ∃ j < i, s j = t}) hm' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>LinearOrder ι<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.iCondIndepSet m' hm' s μ<VAR>i : ι<VAR>k : ι<VAR>hk : i < k<GOAL>ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s k}) (MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}) hm' μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.iCondIndepSet m' hm' s μ<VAR>n : ℕ<GOAL>ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s (n + 1)}) (MeasurableSpace.generateFrom {t | ∃ k ≤ n, s k = t}) hm' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' m₁ mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>SemilatticeSup ι<VAR>m : ι → MeasurableSpace Ω<VAR>h_indep : ∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm' μ<VAR>h_le : ∀ (i : ι), m i ≤ mΩ<VAR>h_le' : m₁ ≤ mΩ<VAR>hm : Monotone m<GOAL>ProbabilityTheory.CondIndep m' (⨆ i, m i) m₁ hm' μ