ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<VAR>this : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω<VAR>ω : Ω<VAR>hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal<GOAL>{ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop} ω = Set.univ ω
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<VAR>this : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω<VAR>ω : Ω<VAR>hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal<GOAL>Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<VAR>this : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω<VAR>ω : Ω<VAR>hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal<GOAL>Tendsto (fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal) atTop atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<VAR>this : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω<VAR>ω : Ω<VAR>hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal<VAR>htends : Tendsto (fun n => ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 ⊤)<GOAL>Tendsto (fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal) atTop atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<VAR>this : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω<VAR>ω : Ω<VAR>hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal<VAR>htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))<GOAL>Tendsto (fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal) atTop atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<VAR>this : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω<VAR>ω : Ω<VAR>hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal<VAR>htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))<GOAL>Monotone fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<VAR>this : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω<VAR>ω : Ω<VAR>hω : ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (μ (s (n + 1))).toReal<VAR>htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))<GOAL>¬BddAbove (Set.range fun n => ∑ x ∈ Finset.range n, (μ (s (x + 1))).toReal)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>x : E<GOAL>gauge 0 x = 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>x : E<GOAL>sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<GOAL>sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ 0} = 0 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>x : E<VAR>hx : x ≠ 0<GOAL>sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ ≠ p₂ ∨ p₃ = p₂<GOAL>0 < ∠ p₂ p₃ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₁ ≠ p₂ ∨ p₃ = p₂<GOAL>0 < ∠ p₂ p₃ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0<GOAL>0 < ∠ p₂ p₃ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0<GOAL>0 < InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯<GOAL>o.bsup f = o.blsub f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯<GOAL>∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f
<VAR>V : Type u<VAR>inst✝ : Quiver V<VAR>a✝¹ b c d a x✝ b✝ : V<VAR>p : Path a b✝<VAR>a✝ : b✝ ⟶ x✝<GOAL>nil.comp (p.cons a✝) = p.cons a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>f g : ι → ℝ≥0∞<VAR>h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k<GOAL>iSup f + iSup g = ⨆ a, f a + g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>f g : ι → ℝ≥0∞<VAR>h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k<VAR>h✝ : IsEmpty ι<GOAL>iSup f + iSup g = ⨆ a, f a + g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>f g : ι → ℝ≥0∞<VAR>h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k<VAR>h✝ : Nonempty ι<GOAL>iSup f + iSup g = ⨆ a, f a + g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s t : Set α<VAR>f : α → β<VAR>a b : α<GOAL>f '' {a, b} = {f a, f b}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>fs : Finset (Fin (n + 1))<GOAL>centroid ℝ fs s.points = (affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter fs)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>fs : Finset (Fin (n + 1))<GOAL>∑ x : Fin (n + 1), (if x ∈ ↑fs then Function.const (Fin (n + 1)) (↑fs.card)⁻¹ x else 0) • (s.points x -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯ = ∑ x : Fin (n + 1), (if x ∈ fs then (↑fs.card)⁻¹ else 0) • (s.points x -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>TendstoUniformlyOn f g atTop (s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>∀ ε_1 > 0, ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg, dist (g x) (f n x) < ε_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>δ : ℝ<VAR>hδ : δ > 0<GOAL>∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg, dist (g x) (f n x) < δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>δ : ℝ<VAR>hδ : δ > 0<VAR>N : ℕ<VAR>hN : 1 / (↑N + 1) < δ<GOAL>∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg, dist (g x) (f n x) < δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>δ : ℝ<VAR>hδ : δ > 0<VAR>N : ℕ<VAR>hN : 1 / (↑N + 1) < δ<GOAL>∃ a, ∀ b ≥ a, ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg, dist (g x) (f b x) < δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>δ : ℝ<VAR>hδ : δ > 0<VAR>N : ℕ<VAR>hN : 1 / (↑N + 1) < δ<VAR>n : ι<VAR>hn : n ≥ notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg N<VAR>x : α<VAR>hx : x ∈ s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg<GOAL>dist (g x) (f n x) < δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>δ : ℝ<VAR>hδ : δ > 0<VAR>N : ℕ<VAR>hN : 1 / (↑N + 1) < δ<VAR>n : ι<VAR>hn : n ≥ notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg N<VAR>x : α<VAR>hx : x ∈ s ∧ (x ∈ s → ∀ (x_1 : ℕ), x ∉ notConvergentSeq f g x_1 (notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg x_1))<GOAL>dist (g x) (f n x) < δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>δ : ℝ<VAR>hδ : δ > 0<VAR>N : ℕ<VAR>hN : 1 / (↑N + 1) < δ<VAR>n : ι<VAR>hn : n ≥ notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg N<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : x ∉ notConvergentSeq f g N (notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg N)<GOAL>dist (g x) (f n x) < δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>δ : ℝ<VAR>hδ : δ > 0<VAR>N : ℕ<VAR>hN : 1 / (↑N + 1) < δ<VAR>n : ι<VAR>hn : n ≥ notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg N<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : ¬∃ k ≥ notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg N, 1 / (↑N + 1) < dist (f k x) (g x)<GOAL>dist (g x) (f n x) < δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>δ : ℝ<VAR>hδ : δ > 0<VAR>N : ℕ<VAR>hN : 1 / (↑N + 1) < δ<VAR>n : ι<VAR>hn : n ≥ notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg N<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : ∀ k ≥ notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg N, dist (f k x) (g x) ≤ 1 / (↑N + 1)<GOAL>dist (g x) (f n x) < δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>δ : ℝ<VAR>hδ : δ > 0<VAR>N : ℕ<VAR>hN : 1 / (↑N + 1) < δ<VAR>n : ι<VAR>hn : n ≥ notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg N<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : ∀ k ≥ notConvergentSeqLTIndex ⋯ hf hg hsm hs hfg N, dist (f k x) (g x) ≤ 1 / (↑N + 1)<GOAL>dist (f n x) (g x) < δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<VAR>h : s ⊆ t<GOAL>s.sym2 ⊆ t.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<VAR>h : s ⊆ t<GOAL>s.val.sym2 ≤ t.val.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<VAR>h : s ⊆ t<GOAL>s.val ≤ t.val
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>↑N = ⊤ ↔ N = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝⁴ : SMul M α<VAR>inst✝³ : SMul N α<VAR>inst✝² : SMul M β<VAR>inst✝¹ : SMul N β<VAR>inst✝ : SMulCommClass M N β<VAR>f : α → β<VAR>hf : Injective f<VAR>h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x<VAR>h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x<VAR>c₁ : M<VAR>c₂ : N<VAR>x : α<GOAL>f (c₁ • c₂ • x) = f (c₂ • c₁ • x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f g : E → F<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hg : ContDiffAt 𝕜 n g x<GOAL>ContDiffAt 𝕜 n (fun x => f x - g x) x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>s : Finset P<GOAL>centroid k univ Subtype.val = centroid k s id
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>s : Finset P<GOAL>(affineCombination k univ Subtype.val) (centroidWeights k univ) = (affineCombination k s.attach Subtype.val) (centroidWeights k s ∘ Subtype.val)
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>P24 x₁ x₂ y ↔ P24 x₁ x₂ (-y)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrder ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n m : ι<VAR>ω : Ω<VAR>h : ∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>stoppedValue u (hitting u s n m) ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrder ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n m : ι<VAR>ω : Ω<VAR>h : ∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrder ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n m : ι<VAR>ω : Ω<VAR>j : ι<VAR>hj₁ : j ∈ Set.Icc n m<VAR>hj₂ : u j ω ∈ s<GOAL>u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrder ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n m : ι<VAR>ω : Ω<VAR>j : ι<VAR>hj₁ : j ∈ Set.Icc n m<VAR>hj₂ : u j ω ∈ s<VAR>this : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s}<GOAL>u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
<VAR>x : ℝ<GOAL>cos (π / 6) = √3 / 2
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν'✝ : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>ν' : Measure β<VAR>inst✝ : SFinite ν'<GOAL>μ.prod (ν + ν') = μ.prod ν + μ.prod ν'
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν'✝ : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>ν' : Measure β<VAR>inst✝ : SFinite ν'<GOAL>(sum fun p => (sFiniteSeq μ p.1).prod (sFiniteSeq ν p.2 + sFiniteSeq ν' p.2)) = sum fun n => (sFiniteSeq μ n.1).prod (sFiniteSeq ν n.2) + (sFiniteSeq μ n.1).prod (sFiniteSeq ν' n.2)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν'✝ : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>ν' : Measure β<VAR>inst✝ : SFinite ν'<VAR>i : ℕ × ℕ<GOAL>(sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2 + sFiniteSeq ν' i.2) = (sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2) + (sFiniteSeq μ i.1).prod (sFiniteSeq ν' i.2)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν'✝ : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>ν' : Measure β<VAR>inst✝ : SFinite ν'<VAR>i : ℕ × ℕ<VAR>s : Set α<VAR>t : Set β<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : MeasurableSet t<GOAL>((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2) + (sFiniteSeq μ i.1).prod (sFiniteSeq ν' i.2)) (s ×ˢ t) = (sFiniteSeq μ i.1) s * (sFiniteSeq ν i.2 + sFiniteSeq ν' i.2) t
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<GOAL>↑a ^ (p / 2) * ↑(p / 2)! = ↑(∏ x ∈ Ico 1 (p / 2).succ, a * ↑x)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<GOAL>↑a ^ (p / 2) * ↑(p / 2)! = ↑(a ^ (p / 2) * ↑(p / 2)!)