ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x y : WittVector p R<VAR>i : ℕ<GOAL>(⇑WittVector.verschiebung)^[i] x * y = (⇑WittVector.verschiebung)^[i] (x * (⇑WittVector.frobenius)^[i] y)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>x y : WittVector p R<VAR>i j : ℕ<GOAL>(⇑WittVector.verschiebung)^[i] x * (⇑WittVector.verschiebung)^[j] y = (⇑WittVector.verschiebung)^[i + j] ((⇑WittVector.frobenius)^[j] x * (⇑WittVector.frobenius)^[i] y)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>x : WittVector p R<VAR>i k : ℕ<GOAL>((⇑WittVector.frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>x y : WittVector p R<VAR>i j : ℕ<GOAL>((⇑WittVector.verschiebung)^[i] x * (⇑WittVector.verschiebung)^[j] y).coeff (i + j) = x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>π : ι → Set (Set Ω)<VAR>h : ProbabilityTheory.Kernel.iIndepSets π κ μ<VAR>s : Finset ι<VAR>f : ι → Set Ω<VAR>hf : ∀ i ∈ s, f i ∈ π i<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>π : ι → Set (Set Ω)<VAR>s : ι → Set Ω<VAR>Fintype ι<VAR>h : ProbabilityTheory.Kernel.iIndepSets π κ μ<VAR>hs : ∀ (i : ι), s i ∈ π i<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>hμ : ProbabilityTheory.Kernel.iIndep m κ μ<GOAL>ProbabilityTheory.Kernel.iIndepSets (fun x => {s | MeasurableSet s}) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set Ω<VAR>S : Finset ι<VAR>hμ : ProbabilityTheory.Kernel.iIndep m κ μ<VAR>hs : ∀ i ∈ S, MeasurableSet (s i)<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set Ω<VAR>Fintype ι<VAR>h : ProbabilityTheory.Kernel.iIndep m κ μ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>mβ : (i : ι) → MeasurableSpace (β i)<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>f : (x : ι) → Ω → β x<VAR>hf : ProbabilityTheory.Kernel.iIndepFun mβ f κ μ<GOAL>ProbabilityTheory.Kernel.iIndep (fun x => MeasurableSpace.comap (f x) (mβ x)) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>mβ : (i : ι) → MeasurableSpace (β i)<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set Ω<VAR>S : Finset ι<VAR>f : (x : ι) → Ω → β x<VAR>hf : ProbabilityTheory.Kernel.iIndepFun mβ f κ μ<VAR>hs : ∀ i ∈ S, MeasurableSet (s i)<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>mβ : (i : ι) → MeasurableSpace (β i)<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>s : ι → Set Ω<VAR>f : (x : ι) → Ω → β x<VAR>Fintype ι<VAR>hf : ProbabilityTheory.Kernel.iIndepFun mβ f κ μ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>γ : Type u_6<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : Ω → β<VAR>g : Ω → γ<VAR>hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>s₁ s₂ : Set (Set Ω)<VAR>h : ProbabilityTheory.Kernel.IndepSets s₁ s₂ κ μ<GOAL>ProbabilityTheory.Kernel.IndepSets s₂ s₁ κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m₁ m₂ _mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h : ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ<GOAL>ProbabilityTheory.Kernel.Indep m₂ m₁ κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m' : MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<GOAL>ProbabilityTheory.Kernel.Indep m' ⊥ κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m' : MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<GOAL>ProbabilityTheory.Kernel.Indep ⊥ m' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>s : Set Ω<GOAL>ProbabilityTheory.Kernel.IndepSet s ∅ κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>s : Set Ω<GOAL>ProbabilityTheory.Kernel.IndepSet ∅ s κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>s₁ s₂ s₃ : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h_indep : ProbabilityTheory.Kernel.IndepSets s₁ s₂ κ μ<VAR>h31 : s₃ ⊆ s₁<GOAL>ProbabilityTheory.Kernel.IndepSets s₃ s₂ κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>s₁ s₂ s₃ : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h_indep : ProbabilityTheory.Kernel.IndepSets s₁ s₂ κ μ<VAR>h32 : s₃ ⊆ s₂<GOAL>ProbabilityTheory.Kernel.IndepSets s₁ s₃ κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m₁ m₂ m₃ _mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h_indep : ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ<VAR>h31 : m₃ ≤ m₁<GOAL>ProbabilityTheory.Kernel.Indep m₃ m₂ κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m₁ m₂ m₃ _mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h_indep : ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ<VAR>h32 : m₃ ≤ m₂<GOAL>ProbabilityTheory.Kernel.Indep m₁ m₃ κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>s₁ s₂ s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h₁ : ProbabilityTheory.Kernel.IndepSets s₁ s' κ μ<VAR>h₂ : ProbabilityTheory.Kernel.IndepSets s₂ s' κ μ<GOAL>ProbabilityTheory.Kernel.IndepSets (s₁ ∪ s₂) s' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>s₁ s₂ s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<GOAL>ProbabilityTheory.Kernel.IndepSets (s₁ ∪ s₂) s' κ μ ↔ ProbabilityTheory.Kernel.IndepSets s₁ s' κ μ ∧ ProbabilityTheory.Kernel.IndepSets s₂ s' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>hyp : ∀ (n : ι), ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ<GOAL>ProbabilityTheory.Kernel.IndepSets (⋃ n, s n) s' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>u : Set ι<VAR>hyp : ∀ n ∈ u, ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ<GOAL>ProbabilityTheory.Kernel.IndepSets (⋃ n ∈ u, s n) s' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>s₁ s' : Set (Set Ω)<VAR>s₂ : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h₁ : ProbabilityTheory.Kernel.IndepSets s₁ s' κ μ<GOAL>ProbabilityTheory.Kernel.IndepSets (s₁ ∩ s₂) s' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h : ∃ n, ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ<GOAL>ProbabilityTheory.Kernel.IndepSets (⋂ n, s n) s' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>u : Set ι<VAR>h : ∃ n ∈ u, ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ<GOAL>ProbabilityTheory.Kernel.IndepSets (⋂ n ∈ u, s n) s' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>f : ι → Set Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<GOAL>ProbabilityTheory.Kernel.iIndep (fun i => MeasurableSpace.comap (fun x => x ∈ f i) ⊤) κ μ ↔ ProbabilityTheory.Kernel.iIndepSet f κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<GOAL>ProbabilityTheory.Kernel.iIndepSets (fun i => {s i}) κ μ ↔ ∀ (S : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>s t : Set Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<GOAL>ProbabilityTheory.Kernel.IndepSets {s} {t} κ μ ↔ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h_indep : ProbabilityTheory.Kernel.iIndepSets s κ μ<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>ProbabilityTheory.Kernel.IndepSets (s i) (s j) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h_indep : ProbabilityTheory.Kernel.iIndep m κ μ<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>ProbabilityTheory.Kernel.Indep (m i) (m j) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : ι → Type u_4<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (i : ι) → Ω → β i<VAR>hf_Indep : ProbabilityTheory.Kernel.iIndepFun m f κ μ<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>ProbabilityTheory.Kernel.IndepFun (f i) (f j) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>m : ι → MeasurableSpace Ω<VAR>s : ι → Set (Set Ω)<VAR>hms : ∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)<VAR>h_indep : ProbabilityTheory.Kernel.iIndep m κ μ<GOAL>ProbabilityTheory.Kernel.iIndepSets s κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>s1 s2 : Set (Set Ω)<VAR>h_indep : ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) κ μ<GOAL>ProbabilityTheory.Kernel.IndepSets s1 s2 κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m₂ m : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h2 : m₂ ≤ m<VAR>hp2 : IsPiSystem p2<VAR>hpm2 : m₂ = MeasurableSpace.generateFrom p2<VAR>hyp : ProbabilityTheory.Kernel.IndepSets p1 p2 κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ p1<VAR>ht1m : MeasurableSet t1<VAR>ht2m : MeasurableSet t2<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m1 m2 m : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>p1 p2 : Set (Set Ω)<VAR>h1 : m1 ≤ m<VAR>h2 : m2 ≤ m<VAR>hp1 : IsPiSystem p1<VAR>hp2 : IsPiSystem p2<VAR>hpm1 : m1 = MeasurableSpace.generateFrom p1<VAR>hpm2 : m2 = MeasurableSpace.generateFrom p2<VAR>hyp : ProbabilityTheory.Kernel.IndepSets p1 p2 κ μ<GOAL>ProbabilityTheory.Kernel.Indep m1 m2 κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<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.Kernel.IndepSets p1 p2 κ μ<GOAL>ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom p1) (MeasurableSpace.generateFrom p2) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>s : ι → Set (Set Ω)<VAR>S T : Set ι<VAR>h_indep : ProbabilityTheory.Kernel.iIndepSets s κ μ<VAR>hST : Disjoint S T<GOAL>ProbabilityTheory.Kernel.IndepSets (piiUnionInter s S) (piiUnionInter s T) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.Kernel.iIndepSet s κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom {t | ∃ n ∈ S, s n = t}) (MeasurableSpace.generateFrom {t | ∃ k ∈ T, s k = t}) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>m : ι → MeasurableSpace Ω<VAR>h_le : ∀ (i : ι), m i ≤ _mΩ<VAR>h_indep : ProbabilityTheory.Kernel.iIndep m κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>ProbabilityTheory.Kernel.Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), ProbabilityTheory.Kernel.Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<GOAL>ProbabilityTheory.Kernel.Indep (⨆ i, m i) m' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>Preorder ι<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.Kernel.iIndepSet s κ μ<VAR>i : ι<GOAL>ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom {s i}) (MeasurableSpace.generateFrom {t | ∃ j < i, s j = t}) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>LinearOrder ι<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.Kernel.iIndepSet s κ μ<VAR>i : ι<VAR>k : ι<VAR>hk : i < k<GOAL>ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom {s k}) (MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.Kernel.iIndepSet s κ μ<VAR>n : ℕ<GOAL>ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom {s (n + 1)}) (MeasurableSpace.generateFrom {t | ∃ k ≤ n, s k = t}) κ μ
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>SemilatticeSup ι<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), ProbabilityTheory.Kernel.Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Monotone m<GOAL>ProbabilityTheory.Kernel.Indep (⨆ i, m i) m' κ μ
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>SemilatticeInf ι<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), ProbabilityTheory.Kernel.Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Antitone m<GOAL>ProbabilityTheory.Kernel.Indep (⨆ i, m i) m' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>π : ι → Set (Set Ω)<VAR>a : ι<VAR>S : Finset ι<VAR>hp_ind : ProbabilityTheory.Kernel.iIndepSets π κ μ<VAR>haS : a ∉ S<GOAL>ProbabilityTheory.Kernel.IndepSets (piiUnionInter π ↑S) (π a) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>m : ι → MeasurableSpace Ω<VAR>h_le : ∀ (i : ι), m i ≤ _mΩ<VAR>π : ι → Set (Set Ω)<VAR>h_pi : ∀ (n : ι), IsPiSystem (π n)<VAR>h_generate : ∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)<VAR>h_ind : ProbabilityTheory.Kernel.iIndepSets π κ μ<GOAL>ProbabilityTheory.Kernel.iIndep m κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → Set Ω<VAR>hf : ∀ (i : ι), MeasurableSet (f i)<GOAL>ProbabilityTheory.Kernel.iIndepSet f κ μ ↔ ProbabilityTheory.Kernel.iIndepSets (fun i => {f i}) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → Set Ω<VAR>hf : ∀ (i : ι), MeasurableSet (f i)<GOAL>ProbabilityTheory.Kernel.iIndepSet f κ μ ↔ ∀ (s : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>μ : MeasureTheory.Measure α<VAR>π : ι → Set (Set Ω)<VAR>f : ι → Set Ω<VAR>hfπ : ∀ (i : ι), f i ∈ π i<VAR>hf : ∀ (i : ι), MeasurableSet (f i)<VAR>hπ : ProbabilityTheory.Kernel.iIndepSets π κ μ<GOAL>ProbabilityTheory.Kernel.iIndepSet f κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>s t : Set Ω<VAR>m0 : MeasurableSpace Ω<VAR>hs_meas : MeasurableSet s<VAR>ht_meas : MeasurableSet t<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<GOAL>ProbabilityTheory.Kernel.IndepSet s t κ μ ↔ ProbabilityTheory.Kernel.IndepSets {s} {t} κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>s t : Set Ω<VAR>_m0 : MeasurableSpace Ω<VAR>hs_meas : MeasurableSet s<VAR>ht_meas : MeasurableSet t<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<GOAL>ProbabilityTheory.Kernel.IndepSet s t κ μ ↔ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>s t : Set Ω<VAR>S T : Set (Set Ω)<VAR>_m0 : MeasurableSpace Ω<VAR>hs : s ∈ S<VAR>ht : t ∈ T<VAR>hs_meas : MeasurableSet s<VAR>ht_meas : MeasurableSet t<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>h_indep : ProbabilityTheory.Kernel.IndepSets S T κ μ<GOAL>ProbabilityTheory.Kernel.IndepSet s t κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m₁ m₂ m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>h_indep : ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>ProbabilityTheory.Kernel.IndepSet s t κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m₁ m₂ : MeasurableSpace Ω<VAR>_m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<GOAL>ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ ↔ ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → ProbabilityTheory.Kernel.IndepSet s t κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<GOAL>ProbabilityTheory.Kernel.IndepFun f g κ μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_8<VAR>β : ι → Type u_9<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (i : ι) → Ω → β i<GOAL>ProbabilityTheory.Kernel.iIndepFun m f κ μ ↔ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>ProbabilityTheory.Kernel.IndepFun f g κ μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → ProbabilityTheory.Kernel.IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<GOAL>∀ {x : MeasurableSpace β} {x_1 : MeasurableSpace β'}, ProbabilityTheory.Kernel.IndepFun f g κ μ → ProbabilityTheory.Kernel.IndepFun g f κ μ