ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>n : ℕ<VAR>hn : n < f.natDegree<VAR>i : ℕ<GOAL>h.coeff (h.root ^ n) i = Pi.single n 1 i
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>n : ℕ<VAR>hn : n < f.natDegree<VAR>i : ℕ<GOAL>(if hi : i < f.natDegree then (h.basis.repr (h.root ^ n)) ⟨i, hi⟩ else 0) = Pi.single n 1 i
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<GOAL>IsUnramified k w ↔ w.IsReal ∨ (w.comap (algebraMap k K)).IsComplex
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>(let_fun h5 := ⋯; preNormEDS' b c d ((2 * m + 1) / 2 + 2) ^ 2 * preNormEDS' b c d ((2 * m + 1) / 2 + 3) * preNormEDS' b c d ((2 * m + 1) / 2 + 5) - preNormEDS' b c d ((2 * m + 1) / 2 + 1) * preNormEDS' b c d ((2 * m + 1) / 2 + 3) * preNormEDS' b c d ((2 * m + 1) / 2 + 4) ^ 2) = preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) - preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>preNormEDS' b c d (m + 1 / 2 + 2) ^ 2 * preNormEDS' b c d (m + 1 / 2 + 3) * preNormEDS' b c d (m + 1 / 2 + 5) - preNormEDS' b c d (m + 1 / 2 + 1) * preNormEDS' b c d (m + 1 / 2 + 3) * preNormEDS' b c d (m + 1 / 2 + 4) ^ 2 = preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) - preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Finset E<GOAL>IsCompactElement (adjoin F ↑S)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Finset E<GOAL>IsCompactElement (⨆ x ∈ ↑S, F⟮x⟯)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Finset E<GOAL>IsCompactElement (S.sup fun a => F⟮a⟯)
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>h : T.IsComplete<VAR>φ : L.Sentence<GOAL>T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>h : T.IsComplete<VAR>φ : L.Sentence<VAR>hφ : T ⊨ᵇ φ<GOAL>T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>h : T.IsComplete<VAR>φ : L.Sentence<VAR>hφn : T ⊨ᵇ Formula.not φ<GOAL>T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : FiniteDimensional ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>f' : E ≃L[ℝ] F<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹<GOAL>∃ g, EqOn f (⇑g) s
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : FiniteDimensional ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>f' : E ≃L[ℝ] F<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹<VAR>u : E → F<VAR>hu : LipschitzWith (lipschitzExtensionConstant F * c) u<VAR>uf : EqOn (f - ⇑f') u s<GOAL>∃ g, EqOn f (⇑g) s
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : FiniteDimensional ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>f' : E ≃L[ℝ] F<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹<VAR>u : E → F<VAR>hu : LipschitzWith (lipschitzExtensionConstant F * c) u<VAR>uf : EqOn (f - ⇑f') u s<VAR>g : E → F := fun x => f' x + u x<GOAL>∃ g, EqOn f (⇑g) s
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : FiniteDimensional ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>f' : E ≃L[ℝ] F<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹<VAR>u : E → F<VAR>hu : LipschitzWith (lipschitzExtensionConstant F * c) u<VAR>uf : EqOn (f - ⇑f') u s<VAR>g : E → F := fun x => f' x + u x<VAR>fg : EqOn f g s<GOAL>∃ g, EqOn f (⇑g) s
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : FiniteDimensional ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>f' : E ≃L[ℝ] F<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹<VAR>u : E → F<VAR>hu : LipschitzWith (lipschitzExtensionConstant F * c) u<VAR>uf : EqOn (f - ⇑f') u s<VAR>g : E → F := fun x => f' x + u x<VAR>fg : EqOn f g s<VAR>hg : ApproximatesLinearOn g (↑f') univ (lipschitzExtensionConstant F * c)<GOAL>∃ g, EqOn f (⇑g) s
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : FiniteDimensional ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>f' : E ≃L[ℝ] F<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹<VAR>u : E → F<VAR>hu : LipschitzWith (lipschitzExtensionConstant F * c) u<VAR>uf : EqOn (f - ⇑f') u s<VAR>g : E → F := fun x => f' x + u x<VAR>fg : EqOn f g s<VAR>hg : ApproximatesLinearOn g (↑f') univ (lipschitzExtensionConstant F * c)<VAR>this : FiniteDimensional ℝ E<GOAL>∃ g, EqOn f (⇑g) s
<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>h : s ⊆ t<VAR>a : α<VAR>ha : a ∈ s<GOAL>f a ∈ f '' t
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>m : M<VAR>i : ι<GOAL>(b.toDual m) (b i) = b.equivFun m i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x✝ : (i : ι) × α i<VAR>i j : ι<VAR>a✝ : α i<VAR>a : (i : ι) → α i<VAR>x : ι<VAR>y : α x<GOAL>(⟨x, y⟩ ∈ s.sigma fun i => {a i}) ↔ ⟨x, y⟩ ∈ (fun i => ⟨i, a i⟩) '' s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁸ : OrderedRing 𝕜<VAR>inst✝⁷ : TopologicalSpace E<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>s t : Set E<VAR>x y : E<VAR>inst✝¹ : Nontrivial 𝕜<VAR>inst✝ : DenselyOrdered 𝕜<VAR>hs : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>h : openSegment 𝕜 x y ⊆ frontier s<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁸ : OrderedRing 𝕜<VAR>inst✝⁷ : TopologicalSpace E<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>s t : Set E<VAR>x y : E<VAR>inst✝¹ : Nontrivial 𝕜<VAR>inst✝ : DenselyOrdered 𝕜<VAR>hs : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>h : openSegment 𝕜 x y ⊆ frontier s<VAR>a : 𝕜<VAR>ha₀ : 0 < a<VAR>ha₁ : a < 1<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<GOAL>ContinuousOn f s ↔ Continuous (s.restrict f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<GOAL>(∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ (x : ↑s), ContinuousAt (s.restrict f) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>h : ∀ (x : ↑s), ContinuousAt (s.restrict f) x<VAR>x : α<VAR>xs : x ∈ s<GOAL>ContinuousWithinAt f s x
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ right b<GOAL>(m.1 - 1, m.2) ∈ Finset.erase b m
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ b ∧ (m.1 - 1, m.2) ∈ b<GOAL>(m.1 - 1, m.2) ∈ Finset.erase b m
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ b ∧ (m.1 - 1, m.2) ∈ b<GOAL>(m.1 - 1, m.2) ≠ m
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>(fun n => ε (b i * ↑n) - ε ↑n) ~[atTop] fun n => -log (b i) / log ↑n ^ 2
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<GOAL>-(∡ p₁ p₂ p₃).sign = (∡ p₁ p₃ p₂).sign
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hn : IsPeriodicPt f n x<VAR>hm : IsPeriodicPt f m x<GOAL>IsPeriodicPt f (n + m) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hn : IsPeriodicPt f n x<VAR>hm : IsPeriodicPt f m x<GOAL>IsFixedPt (f^[n] ∘ f^[m]) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<GOAL>univ.card = Fintype.card α
<VAR>α : Type u<VAR>β : α → Type v<VAR>s₁ s₂ : AList β<VAR>h : s₁.entries ⊆ s₂.entries<VAR>k : α<VAR>hk : k ∈ s₁.keys<VAR>this : DecidableEq α := Classical.decEq α<GOAL>k ∈ s₂.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>s₁ s₂ : AList β<VAR>h : s₁.entries ⊆ s₂.entries<VAR>k : α<VAR>hk : k ∈ s₁.keys<VAR>this✝ : DecidableEq α := Classical.decEq α<VAR>this : ⟨k, (lookup k s₁).get ⋯⟩ ∈ s₂.entries<GOAL>k ∈ s₂.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>s₁ s₂ : AList β<VAR>h : s₁.entries ⊆ s₂.entries<VAR>k : α<VAR>hk : k ∈ s₁.keys<VAR>this✝ : DecidableEq α := Classical.decEq α<VAR>this : lookup k s₂ = some ((lookup k s₁).get ⋯)<GOAL>k ∈ s₂.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>s₁ s₂ : AList β<VAR>h : s₁.entries ⊆ s₂.entries<VAR>k : α<VAR>hk : k ∈ s₁.keys<VAR>this✝ : DecidableEq α := Classical.decEq α<VAR>this : lookup k s₂ = some ((lookup k s₁).get ⋯)<GOAL>(some ((lookup k s₁).get ⋯)).isSome = true
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<GOAL>∑ p : n × n, (algebraMap R A) (M p.1 p.2) ⊗ₜ[R] stdBasisMatrix p.1 p.2 1 = 1 ⊗ₜ[R] M
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<GOAL>1 ⊗ₜ[R] ∑ a : n × n, M a.1 a.2 • stdBasisMatrix a.1 a.2 1 = 1 ⊗ₜ[R] M
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<GOAL>∑ a : n × n, M a.1 a.2 • stdBasisMatrix a.1 a.2 1 = M
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<GOAL>∑ a : n × n, M a.1 a.2 • stdBasisMatrix a.1 a.2 1 = ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j)
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<VAR>x✝¹ : n<VAR>a✝¹ : x✝¹ ∈ Finset.univ<VAR>x✝ : n<VAR>a✝ : x✝ ∈ Finset.univ<GOAL>stdBasisMatrix x✝¹ x✝ (M x✝¹ x✝) = M (x✝¹, x✝).1 (x✝¹, x✝).2 • stdBasisMatrix (x✝¹, x✝).1 (x✝¹, x✝).2 1
<VAR>a b : ℝ<VAR>n : ℕ<VAR>h : 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
<VAR>n : Type u<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Subsingleton n<VAR>x : SpecialLinearGroup n R<VAR>x✝ : x ∈ center (SpecialLinearGroup n R)<GOAL>x ∈ ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p q u v x y z : E<VAR>hz : z ∈ segment 𝕜 x y<VAR>hu : u ∈ segment 𝕜 x p<VAR>hv : v ∈ segment 𝕜 y q<GOAL>¬Disjoint (segment 𝕜 u v) ((convexHull 𝕜) {p, q, z})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p q u v x y z : E<VAR>hz : z ∈ segment 𝕜 x y<VAR>hu : u ∈ segment 𝕜 x p<VAR>hv : v ∈ segment 𝕜 y q<GOAL>∃ x ∈ segment 𝕜 u v, x ∈ (convexHull 𝕜) {p, q, z}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p q x y : E<VAR>az bz : 𝕜<VAR>haz : 0 ≤ az<VAR>hbz : 0 ≤ bz<VAR>habz : az + bz = 1<VAR>haz' : 0 < az<VAR>av bv : 𝕜<VAR>hav : 0 ≤ av<VAR>hbv : 0 ≤ bv<VAR>habv : av + bv = 1<VAR>hav' : 0 < av<VAR>au bu : 𝕜<VAR>hau : 0 ≤ au<VAR>hbu : 0 ≤ bu<VAR>habu : au + bu = 1<VAR>hab : 0 < az * av + bz * au<GOAL>(az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) ∈ (convexHull 𝕜) {p, q, az • x + bz • y}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p q x y : E<VAR>az bz : 𝕜<VAR>haz : 0 ≤ az<VAR>hbz : 0 ≤ bz<VAR>habz : az + bz = 1<VAR>haz' : 0 < az<VAR>av bv : 𝕜<VAR>hav : 0 ≤ av<VAR>hbv : 0 ≤ bv<VAR>habv : av + bv = 1<VAR>hav' : 0 < av<VAR>au bu : 𝕜<VAR>hau : 0 ≤ au<VAR>hbu : 0 ≤ bu<VAR>habu : au + bu = 1<VAR>hab : 0 < az * av + bz * au<GOAL>(az * av / (az * av + bz * au) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q + ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) ∈ (convexHull 𝕜) {p, q, az • x + bz • y}
<VAR>a b : ℤ<GOAL>a ≠ b ↔ ↑a ≠ ↑b
<VAR>ι : Sort u_1<VAR>f✝ g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_2<VAR>f : ι → α → ℝ≥0∞<VAR>s : Finset α<VAR>inst✝ : Nonempty ι<VAR>h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a<GOAL>⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
<VAR>ι : Sort u_1<VAR>f✝ g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_2<VAR>f : ι → α → ℝ≥0∞<VAR>inst✝ : Nonempty ι<VAR>h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a<GOAL>⨅ i, ∑ a ∈ ∅, f i a = ∑ a ∈ ∅, ⨅ i, f i a
<VAR>ι : Sort u_1<VAR>f✝ g : ι → ℝ≥0∞<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_2<VAR>f : ι → α → ℝ≥0∞<VAR>inst✝ : Nonempty ι<VAR>h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a<GOAL>⨅ i, ∑ a ∈ Finset.cons a s ha, f i a = ∑ a ∈ Finset.cons a s ha, ⨅ i, f i a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>α' : Type u_7<VAR>α'' : Type u_8<VAR>f : α → α'<VAR>s : Set α'<GOAL>supported M R (f ⁻¹' s) ≤ comap (lmapDomain M R f) (supported M R s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : α → ℝ<VAR>h_meas : AEStronglyMeasurable f μ<VAR>hf : f ≤ᶠ[ae μ] 0<VAR>hg : g ≤ᶠ[ae μ] 0<GOAL>Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : α → ℝ<VAR>h_meas : AEStronglyMeasurable f μ<VAR>hf : f ≤ᶠ[ae μ] 0<VAR>hg : g ≤ᶠ[ae μ] 0<GOAL>Integrable (-f + -g) μ ↔ Integrable (-f) μ ∧ Integrable (-g) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>K : Set X<VAR>a b : X<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>hK : IsCompact K<VAR>h'K : MeasurableSet K<VAR>hf : ContinuousOn f K<GOAL>IntegrableOn f K μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>K : Set X<VAR>a b : X<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>hK : IsCompact K<VAR>h'K : MeasurableSet K<VAR>hf : ContinuousOn f K<GOAL>HasFiniteIntegral f (μ.restrict K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>K : Set X<VAR>a b : X<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>hK : IsCompact K<VAR>h'K : MeasurableSet K<VAR>hf : ContinuousOn f K<VAR>this : Fact (μ K < ⊤)<GOAL>HasFiniteIntegral f (μ.restrict K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>K : Set X<VAR>a b : X<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>hK : IsCompact K<VAR>h'K : MeasurableSet K<VAR>hf : ContinuousOn f K<VAR>this : Fact (μ K < ⊤)<VAR>C : ℝ<VAR>hC : ∀ x ∈ f '' K, ‖x‖ ≤ C<GOAL>HasFiniteIntegral f (μ.restrict K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>K : Set X<VAR>a b : X<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>hK : IsCompact K<VAR>h'K : MeasurableSet K<VAR>hf : ContinuousOn f K<VAR>this : Fact (μ K < ⊤)<VAR>C : ℝ<VAR>hC : ∀ x ∈ f '' K, ‖x‖ ≤ C<GOAL>∀ᵐ (a : X) ∂μ.restrict K, ‖f a‖ ≤ C
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>h : CG L M<VAR>f : M →[L] N<VAR>hs : Function.Surjective ⇑f<GOAL>CG L N
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>h : CG L M<VAR>f : M →[L] N<VAR>hs : f.range = ⊤<GOAL>CG L N
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>h : CG L M<VAR>f : M →[L] N<VAR>hs : f.range = ⊤<GOAL>f.range.CG
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>(mapL f) x = (map fun i => ↑(f i)) x
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>r✝ : 𝕜<VAR>f✝ : (i : ι) → E i<GOAL>(mapL f) (r✝ • (tprod 𝕜) f✝) = (map fun i => ↑(f i)) (r✝ • (tprod 𝕜) f✝)
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x✝ y✝ : ⨂[𝕜] (i : ι), E i<VAR>hx : (mapL f) x✝ = (map fun i => ↑(f i)) x✝<VAR>hy : (mapL f) y✝ = (map fun i => ↑(f i)) y✝<GOAL>(mapL f) (x✝ + y✝) = (map fun i => ↑(f i)) (x✝ + y✝)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑(sa * s₁) = ra * ↑s₂<GOAL>(r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) = (r₃ /ₒ s₃) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₂ /ₒ s₂)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑(sa * s₁) = ra * ↑s₂<GOAL>(r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) = (r₃ /ₒ s₃) • (sa • r₁ /ₒ (sa * s₁)) + (r₃ /ₒ s₃) • (r₂ /ₒ s₂)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑(sa * s₁) = ra * ↑s₂<GOAL>(r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) = (r₃ /ₒ s₃) • (sa • r₁ /ₒ (sa * s₁)) + (r₃ /ₒ s₃) • (ra • r₂ /ₒ ⟨ra * ↑s₂, ⋯⟩)