ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → List β<VAR>g : α → β → σ<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<GOAL>Primrec fun a => List.map (g a) (f a)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec List.join
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → List β<VAR>g : α → β → List σ<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<GOAL>Primrec fun a => (f a).bind (g a)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec Option.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → List β<VAR>g : α → β → Option σ<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<GOAL>Primrec fun a => List.filterMap (g a) (f a)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec List.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → List β<VAR>p : α → β → Bool<VAR>hf : Primrec f<VAR>hp : Primrec₂ p<GOAL>Primrec fun a => List.findIdx (p a) (f a)
<VAR>α : Type u_1<VAR>Primcodable α<VAR>DecidableEq α<GOAL>Primrec₂ List.indexOf
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → ℕ → σ<VAR>g : α → List σ → Option σ<VAR>hg : Primrec₂ g<VAR>H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)<GOAL>Primrec₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>DecidableEq α<GOAL>Primrec₂ List.lookup
<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : β → σ<VAR>m : β → ℕ<VAR>l : β → List β<VAR>g : β → List σ → Option σ<VAR>hm : Primrec m<VAR>hl : Primrec l<VAR>hg : Primrec₂ g<VAR>Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b<VAR>H : ∀ (b : β), g b (List.map f (l b)) = some (f b)<GOAL>Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<VAR>m : α → β → ℕ<VAR>l : α → β → List β<VAR>g : α → β × List σ → Option σ<VAR>hm : Primrec₂ m<VAR>hl : Primrec₂ l<VAR>hg : Primrec₂ g<VAR>Ord : ∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b<VAR>H : ∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)<GOAL>Primrec₂ f
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>PrimrecPred fun n => n ∈ Set.range Encodable.encode
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hp : PrimrecPred p<GOAL>Primrec Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : β → Prop<VAR>DecidablePred p<VAR>hp : PrimrecPred p<VAR>f : α → Subtype p<GOAL>(Primrec fun a => ↑(f a)) ↔ Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : β → Prop<VAR>DecidablePred p<VAR>hp : PrimrecPred p<VAR>f : α → β<VAR>h : ∀ (a : α), p (f a)<VAR>hf : Primrec f<GOAL>Primrec fun a => ⟨f a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → Option β<VAR>h : ∀ (a : α), (f a).isSome = true<GOAL>Primrec f → Primrec fun a => (f a).get ⋯
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec ULower.down
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec ULower.up
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<VAR>f : α → Fin n<GOAL>(Primrec fun a => ↑(f a)) ↔ Primrec f
<VAR>n : ℕ<GOAL>Primrec fun i => ↑i
<VAR>n : ℕ<GOAL>Primrec Fin.succ
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Primrec Mathlib.Vector.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>n : ℕ<VAR>f : α → Mathlib.Vector β n<GOAL>(Primrec fun a => (f a).toList) ↔ Primrec f
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Primrec₂ Mathlib.Vector.cons
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Primrec Mathlib.Vector.length
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Primrec Mathlib.Vector.head
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Primrec Mathlib.Vector.tail
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Primrec₂ Mathlib.Vector.get
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>n : ℕ<VAR>f : Fin n → α → σ<GOAL>(∀ (i : Fin n), Primrec (f i)) → Primrec fun a => List.ofFn fun i => f i a
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>n : ℕ<VAR>f : Fin n → α → σ<VAR>hf : ∀ (i : Fin n), Primrec (f i)<GOAL>Primrec fun a => Mathlib.Vector.ofFn fun i => f i a
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Primrec Mathlib.Vector.get
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Primrec Mathlib.Vector.ofFn
<VAR>σ : Type u_4<VAR>Primcodable σ<VAR>n : ℕ<GOAL>Primrec₂ id
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>n : ℕ<VAR>f : Fin n → α → σ<GOAL>Primrec₂ f ↔ ∀ (i : Fin n), Primrec (f i)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>n : ℕ<VAR>f : α → Fin n → σ<GOAL>Primrec f ↔ Primrec₂ f
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n → ℕ<VAR>pf : Nat.Primrec' f<GOAL>Primrec f
<VAR>n : ℕ<VAR>f g : Mathlib.Vector ℕ n → ℕ<VAR>hf : Nat.Primrec' f<VAR>H : ∀ (i : Mathlib.Vector ℕ n), f i = g i<GOAL>Nat.Primrec' g
<VAR>n : ℕ<VAR>m : ℕ<GOAL>Nat.Primrec' fun x => m
<VAR>n : ℕ<GOAL>Nat.Primrec' Mathlib.Vector.head
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n → ℕ<VAR>hf : Nat.Primrec' f<GOAL>Nat.Primrec' fun v => f v.tail
<VAR>n : ℕ<GOAL>Nat.Primrec'.Vec fun x => Mathlib.Vector.nil
<VAR>n m : ℕ<VAR>f : Mathlib.Vector ℕ n → ℕ<VAR>g : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m<VAR>hf : Nat.Primrec' f<VAR>hg : Nat.Primrec'.Vec g<GOAL>Nat.Primrec'.Vec fun v => f v ::ᵥ g v
<VAR>n : ℕ<GOAL>Nat.Primrec'.Vec id
<VAR>n m : ℕ<VAR>f : Mathlib.Vector ℕ m → ℕ<VAR>g : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m<VAR>hf : Nat.Primrec' f<VAR>hg : Nat.Primrec'.Vec g<GOAL>Nat.Primrec' fun v => f (g v)
<VAR>f : ℕ → ℕ<VAR>hf : Nat.Primrec' fun v => f v.head<VAR>n : ℕ<VAR>g : Mathlib.Vector ℕ n → ℕ<VAR>hg : Nat.Primrec' g<GOAL>Nat.Primrec' fun v => f (g v)
<VAR>f : ℕ → ℕ → ℕ<VAR>hf : Nat.Primrec' fun v => f v.head v.tail.head<VAR>n : ℕ<VAR>g h : Mathlib.Vector ℕ n → ℕ<VAR>hg : Nat.Primrec' g<VAR>hh : Nat.Primrec' h<GOAL>Nat.Primrec' fun v => f (g v) (h v)
<VAR>n : ℕ<VAR>f g : Mathlib.Vector ℕ n → ℕ<VAR>h : Mathlib.Vector ℕ (n + 2) → ℕ<VAR>hf : Nat.Primrec' f<VAR>hg : Nat.Primrec' g<VAR>hh : Nat.Primrec' h<GOAL>Nat.Primrec' fun v => Nat.rec (g v) (fun y IH => h (y ::ᵥ IH ::ᵥ v)) (f v)
<GOAL>Nat.Primrec' fun v => v.head + v.tail.head
<GOAL>Nat.Primrec' fun v => v.head - v.tail.head
<GOAL>Nat.Primrec' fun v => v.head * v.tail.head
<VAR>n : ℕ<VAR>a b f g : Mathlib.Vector ℕ n → ℕ<VAR>ha : Nat.Primrec' a<VAR>hb : Nat.Primrec' b<VAR>hf : Nat.Primrec' f<VAR>hg : Nat.Primrec' g<GOAL>Nat.Primrec' fun v => if a v < b v then f v else g v
<GOAL>Nat.Primrec' fun v => Nat.pair v.head v.tail.head
<VAR>n : ℕ<GOAL>Nat.Primrec' Encodable.encode
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n → ℕ<VAR>hf : Nat.Primrec' f<GOAL>Nat.Primrec' fun v => (Nat.unpair (f v)).1
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n → ℕ<VAR>hf : Nat.Primrec' f<GOAL>Nat.Primrec' fun v => (Nat.unpair (f v)).2
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n → ℕ<GOAL>Primrec f → Nat.Primrec' f
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n → ℕ<GOAL>Nat.Primrec' f ↔ Primrec f
<VAR>f : ℕ → ℕ<GOAL>(Nat.Primrec' fun v => f v.head) ↔ Primrec f
<VAR>f : ℕ → ℕ → ℕ<GOAL>(Nat.Primrec' fun v => f v.head v.tail.head) ↔ Primrec₂ f
<VAR>m n : ℕ<VAR>f : Mathlib.Vector ℕ m → Mathlib.Vector ℕ n<GOAL>Nat.Primrec'.Vec f ↔ Primrec f
<VAR>r : ℝ≥0<GOAL>HasSum (fun n => ProbabilityTheory.poissonPMFReal r n) 1
<VAR>r : ℝ≥0<VAR>n : ℕ<VAR>hr : 0 < r<GOAL>0 < ProbabilityTheory.poissonPMFReal r n
<VAR>r : ℝ≥0<VAR>n : ℕ<GOAL>0 ≤ ProbabilityTheory.poissonPMFReal r n
<VAR>r : ℝ≥0<GOAL>Measurable (ProbabilityTheory.poissonPMFReal r)
<VAR>r : ℝ≥0<GOAL>MeasureTheory.StronglyMeasurable (ProbabilityTheory.poissonPMFReal r)
<VAR>p : ℝ<VAR>hp_pos : 0 < p<VAR>hp_le_one : p ≤ 1<GOAL>HasSum (fun n => ProbabilityTheory.geometricPMFReal p n) 1
<VAR>p : ℝ<VAR>n : ℕ<VAR>hp_pos : 0 < p<VAR>hp_lt_one : p < 1<GOAL>0 < ProbabilityTheory.geometricPMFReal p n
<VAR>p : ℝ<VAR>n : ℕ<VAR>hp_pos : 0 < p<VAR>hp_le_one : p ≤ 1<GOAL>0 ≤ ProbabilityTheory.geometricPMFReal p n
<VAR>p : ℝ<GOAL>Measurable (ProbabilityTheory.geometricPMFReal p)
<VAR>p : ℝ<GOAL>MeasureTheory.StronglyMeasurable (ProbabilityTheory.geometricPMFReal p)
<VAR>p : ℝ<VAR>hp_pos : 0 < p<VAR>hp_le_one : p ≤ 1<GOAL>MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.geometricMeasure hp_pos hp_le_one)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} (π : ι → Set (Set Ω)) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.iIndepSets π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set Ω)<GOAL>∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}, ProbabilityTheory.iIndepSets π μ → ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set Ω)<GOAL>∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set Ω} [inst : Fintype ι], ProbabilityTheory.iIndepSets π μ → (∀ (i : ι), s i ∈ π i) → μ (⋂ i, s i) = ∏ i : ι, μ (s i)
<VAR>Ω : Type u_1<GOAL>∀ {x : MeasurableSpace Ω} (s1 s2 : Set (Set Ω)) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.IndepSets s1 s2 μ ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ (t1 ∩ t2) = μ t1 * μ t2
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.iIndep m μ ↔ ProbabilityTheory.iIndepSets (fun x => {s | MeasurableSet s}) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<GOAL>∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}, ProbabilityTheory.iIndep m μ → ProbabilityTheory.iIndepSets (fun x => {s | MeasurableSet s}) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.iIndep m μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<GOAL>∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Finset ι} {s : ι → Set Ω}, ProbabilityTheory.iIndep m μ → (∀ i ∈ S, MeasurableSet (s i)) → μ (⋂ i ∈ S, s i) = ∏ i ∈ S, μ (s i)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<GOAL>∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set Ω} [inst : Fintype ι], ProbabilityTheory.iIndep m μ → (∀ (i : ι), MeasurableSet (s i)) → μ (⋂ i, s i) = ∏ i : ι, μ (s i)
<VAR>Ω : Type u_1<VAR>m₁ m₂ : MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.Indep m₁ m₂ μ ↔ ProbabilityTheory.IndepSets {s | MeasurableSet s} {s | MeasurableSet s} μ
<VAR>Ω : Type u_1<VAR>m₁ m₂ : MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.Indep m₁ m₂ μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
<VAR>Ω : Type u_1<VAR>ι : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} (s : ι → Set Ω) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.iIndepSet s μ ↔ ProbabilityTheory.iIndep (fun i => MeasurableSpace.generateFrom {s i}) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} (s : ι → Set Ω) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.iIndepSet s μ ↔ ∀ (s' : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s', MeasurableSet (f i)) → μ (⋂ i ∈ s', f i) = ∏ i ∈ s', μ (f i)
<VAR>Ω : Type u_1<GOAL>∀ {x : MeasurableSpace Ω} (s t : Set Ω) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.IndepSet s t μ ↔ ProbabilityTheory.Indep (MeasurableSpace.generateFrom {s}) (MeasurableSpace.generateFrom {t}) μ
<VAR>Ω : Type u_1<GOAL>∀ {x : MeasurableSpace Ω} (s t : Set Ω) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.IndepSet s t μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
<VAR>Ω : Type u_1<VAR>ι : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {β : ι → Type u_6} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ω → β x) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.iIndepFun m f μ ↔ ProbabilityTheory.iIndep (fun x => MeasurableSpace.comap (f x) (m x)) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>κ : ι → Type u_5<GOAL>∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ω → κ x}, ProbabilityTheory.iIndepFun m f μ → ProbabilityTheory.iIndep (fun x => MeasurableSpace.comap (f x) (m x)) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {β : ι → Type u_6} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ω → β x) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.iIndepFun m f μ ↔ ∀ (s : Finset ι) {f' : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f' i)) → μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>κ : ι → Type u_5<GOAL>∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Finset ι} {s : ι → Set Ω} {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ω → κ x}, ProbabilityTheory.iIndepFun m f μ → (∀ i ∈ S, MeasurableSet (s i)) → μ (⋂ i ∈ S, s i) = ∏ i ∈ S, μ (s i)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>κ : ι → Type u_5<GOAL>∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set Ω} [inst : Fintype ι] {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ω → κ x}, ProbabilityTheory.iIndepFun m f μ → (∀ (i : ι), MeasurableSet (s i)) → μ (⋂ i, s i) = ∏ i : ι, μ (s i)
<VAR>Ω : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_4<GOAL>∀ {x : MeasurableSpace Ω} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.IndepFun f g μ ↔ ProbabilityTheory.Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ
<VAR>Ω : Type u_1<GOAL>∀ {x : MeasurableSpace Ω} {β : Type u_6} {γ : Type u_7} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : MeasureTheory.Measure Ω), ProbabilityTheory.IndepFun f g μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
<VAR>Ω : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_4<GOAL>∀ {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] {f : Ω → β} {g : Ω → γ}, ProbabilityTheory.IndepFun f g μ → ∀ {s t : Set Ω}, MeasurableSet s → MeasurableSet t → μ (s ∩ t) = μ s * μ t
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s₁ s₂ : Set (Set Ω)<VAR>h : ProbabilityTheory.IndepSets s₁ s₂ μ<GOAL>ProbabilityTheory.IndepSets s₂ s₁ μ
<VAR>Ω : Type u_1<VAR>m₁ m₂ _mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>h : ProbabilityTheory.Indep m₁ m₂ μ<GOAL>ProbabilityTheory.Indep m₂ m₁ μ
<VAR>Ω : Type u_1<VAR>m' : MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>ProbabilityTheory.Indep m' ⊥ μ
<VAR>Ω : Type u_1<VAR>m' : MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>ProbabilityTheory.Indep ⊥ m' μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>s : Set Ω<GOAL>ProbabilityTheory.IndepSet s ∅ μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>s : Set Ω<GOAL>ProbabilityTheory.IndepSet ∅ s μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s₁ s₂ s₃ : Set (Set Ω)<VAR>h_indep : ProbabilityTheory.IndepSets s₁ s₂ μ<VAR>h31 : s₃ ⊆ s₁<GOAL>ProbabilityTheory.IndepSets s₃ s₂ μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s₁ s₂ s₃ : Set (Set Ω)<VAR>h_indep : ProbabilityTheory.IndepSets s₁ s₂ μ<VAR>h32 : s₃ ⊆ s₂<GOAL>ProbabilityTheory.IndepSets s₁ s₃ μ
<VAR>Ω : Type u_1<VAR>m₁ m₂ m₃ _mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>h_indep : ProbabilityTheory.Indep m₁ m₂ μ<VAR>h31 : m₃ ≤ m₁<GOAL>ProbabilityTheory.Indep m₃ m₂ μ
<VAR>Ω : Type u_1<VAR>m₁ m₂ m₃ _mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>h_indep : ProbabilityTheory.Indep m₁ m₂ μ<VAR>h32 : m₃ ≤ m₂<GOAL>ProbabilityTheory.Indep m₁ m₃ μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s₁ s₂ s' : Set (Set Ω)<VAR>h₁ : ProbabilityTheory.IndepSets s₁ s' μ<VAR>h₂ : ProbabilityTheory.IndepSets s₂ s' μ<GOAL>ProbabilityTheory.IndepSets (s₁ ∪ s₂) s' μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s₁ s₂ s' : Set (Set Ω)<GOAL>ProbabilityTheory.IndepSets (s₁ ∪ s₂) s' μ ↔ ProbabilityTheory.IndepSets s₁ s' μ ∧ ProbabilityTheory.IndepSets s₂ s' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>hyp : ∀ (n : ι), ProbabilityTheory.IndepSets (s n) s' μ<GOAL>ProbabilityTheory.IndepSets (⋃ n, s n) s' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>u : Set ι<VAR>hyp : ∀ n ∈ u, ProbabilityTheory.IndepSets (s n) s' μ<GOAL>ProbabilityTheory.IndepSets (⋃ n ∈ u, s n) s' μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s₁ s' : Set (Set Ω)<VAR>s₂ : Set (Set Ω)<VAR>h₁ : ProbabilityTheory.IndepSets s₁ s' μ<GOAL>ProbabilityTheory.IndepSets (s₁ ∩ s₂) s' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>h : ∃ n, ProbabilityTheory.IndepSets (s n) s' μ<GOAL>ProbabilityTheory.IndepSets (⋂ n, s n) s' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>u : Set ι<VAR>h : ∃ n ∈ u, ProbabilityTheory.IndepSets (s n) s' μ<GOAL>ProbabilityTheory.IndepSets (⋂ n ∈ u, s n) s' μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s t : Set Ω<GOAL>ProbabilityTheory.IndepSets {s} {t} μ ↔ μ (s ∩ t) = μ s * μ t
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : ι → Set (Set Ω)<VAR>h_indep : ProbabilityTheory.iIndepSets s μ<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>ProbabilityTheory.IndepSets (s i) (s j) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>h_indep : ProbabilityTheory.iIndep m μ<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>ProbabilityTheory.Indep (m i) (m j) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : ι → Type u_6<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (i : ι) → Ω → β i<VAR>hf_Indep : ProbabilityTheory.iIndepFun m f μ<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>ProbabilityTheory.IndepFun (f i) (f j) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : ι → Set (Set Ω)<VAR>hms : ∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)<VAR>h_indep : ProbabilityTheory.iIndep m μ<GOAL>ProbabilityTheory.iIndepSets s μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s1 s2 : Set (Set Ω)<VAR>h_indep : ProbabilityTheory.Indep (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) μ<GOAL>ProbabilityTheory.IndepSets s1 s2 μ
<VAR>Ω : Type u_1<VAR>m1 m2 _mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<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.IndepSets p1 p2 μ<GOAL>ProbabilityTheory.Indep m1 m2 μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<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.IndepSets p1 p2 μ<GOAL>ProbabilityTheory.Indep (MeasurableSpace.generateFrom p1) (MeasurableSpace.generateFrom p2) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>s : ι → Set (Set Ω)<VAR>S T : Set ι<VAR>h_indep : ProbabilityTheory.iIndepSets s μ<VAR>hST : Disjoint S T<GOAL>ProbabilityTheory.IndepSets (piiUnionInter s S) (piiUnionInter s T) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.iIndepSet s μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>ProbabilityTheory.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>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>h_le : ∀ (i : ι), m i ≤ _mΩ<VAR>h_indep : ProbabilityTheory.iIndep m μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>ProbabilityTheory.Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<VAR>m1 _mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>h_indep : ∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ<VAR>h_le : ∀ (i : ι), m i ≤ _mΩ<VAR>h_le' : m1 ≤ _mΩ<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<GOAL>ProbabilityTheory.Indep (⨆ i, m i) m1 μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>Preorder ι<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.iIndepSet s μ<VAR>i : ι<GOAL>ProbabilityTheory.Indep (MeasurableSpace.generateFrom {s i}) (MeasurableSpace.generateFrom {t | ∃ j < i, s j = t}) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>LinearOrder ι<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.iIndepSet s μ<VAR>i : ι<VAR>k : ι<VAR>hk : i < k<GOAL>ProbabilityTheory.Indep (MeasurableSpace.generateFrom {s k}) (MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}) μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.iIndepSet s μ<VAR>n : ℕ<GOAL>ProbabilityTheory.Indep (MeasurableSpace.generateFrom {s (n + 1)}) (MeasurableSpace.generateFrom {t | ∃ k ≤ n, s k = t}) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<VAR>m1 _mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>SemilatticeSup ι<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>h_indep : ∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ<VAR>h_le : ∀ (i : ι), m i ≤ _mΩ<VAR>h_le' : m1 ≤ _mΩ<VAR>hm : Monotone m<GOAL>ProbabilityTheory.Indep (⨆ i, m i) m1 μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<VAR>m1 _mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>SemilatticeInf ι<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>h_indep : ∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ<VAR>h_le : ∀ (i : ι), m i ≤ _mΩ<VAR>h_le' : m1 ≤ _mΩ<VAR>hm : Antitone m<GOAL>ProbabilityTheory.Indep (⨆ i, m i) m1 μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>π : ι → Set (Set Ω)<VAR>a : ι<VAR>S : Finset ι<VAR>hp_ind : ProbabilityTheory.iIndepSets π μ<VAR>haS : a ∉ S<GOAL>ProbabilityTheory.IndepSets (piiUnionInter π ↑S) (π a) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<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.iIndepSets π μ<GOAL>ProbabilityTheory.iIndep m μ