ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)<VAR>card_K : ℵ₀ < #K<VAR>this✝² : Module.rank K (ℕ → K) < #K<VAR>ιK : Type u<VAR>bK : Basis ιK K (ℕ → K)<VAR>L : Subfield K := Subfield.closure (range fun i => bK i.1 i.2)<VAR>hLK : #↥L < #K<VAR>this✝¹ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)<VAR>ιL : Type u<VAR>bL : Basis ιL (↥L)ᵐᵒᵖ K<VAR>card_ιL : ℵ₀ ≤ #ιL<VAR>e : ℕ ↪ ιL<VAR>t : Finset ℕ<VAR>g : ℕ → (↥L)ᵐᵒᵖ<VAR>i✝ : ℕ<VAR>hi✝ : i✝ ∈ t<VAR>hgi : g i✝ ≠ 0<VAR>s : Finset ιK<VAR>f : ℕ → { x // x ∈ s } → ↥L := fun i j => ⟨bK (↑j) i, ⋯⟩<VAR>this✝ : ¬LinearIndependent (↥L)ᵐᵒᵖ f<VAR>c : ιK →₀ K<VAR>rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e<VAR>i : ιK<VAR>hi : i ∈ s<VAR>eq0 : ∑ x ∈ t, L.subtype ((g x • f x) ⟨i, hi⟩) = L.subtype (0 ⟨i, hi⟩)<VAR>this : SMulCommClass (↥L)ᵐᵒᵖ K K<GOAL>c i • ∑ x ∈ t, g x • bK i x = 0
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<VAR>α' : Type u_3<VAR>inst✝¹ : MeasurableSpace α'<VAR>β' : Type u_4<VAR>inst✝ : MeasurableSpace β'<VAR>f : α → α'<VAR>g : β → β'<VAR>f_mble : Measurable f<VAR>g_mble : Measurable g<GOAL>(μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g)
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<VAR>α' : Type u_3<VAR>inst✝¹ : MeasurableSpace α'<VAR>β' : Type u_4<VAR>inst✝ : MeasurableSpace β'<VAR>f : α → α'<VAR>g : β → β'<VAR>f_mble : Measurable f<VAR>g_mble : Measurable g<GOAL>↑((μ.map f).prod (ν.map g)) = ↑((μ.prod ν).map (Prod.map f g))
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<VAR>α' : Type u_3<VAR>inst✝¹ : MeasurableSpace α'<VAR>β' : Type u_4<VAR>inst✝ : MeasurableSpace β'<VAR>f : α → α'<VAR>g : β → β'<VAR>f_mble : Measurable f<VAR>g_mble : Measurable g<GOAL>(Measure.map f ↑μ).prod (Measure.map g ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>biprod.inl.f i ≫ biprod.fst.f i = 𝟙 (K.X i)
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>p : ℝ<VAR>ι : Type := Fin (finrank ℝ E)<GOAL>ℝ≥0
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>p : ℝ<VAR>ι : Type := Fin (finrank ℝ E)<VAR>this : finrank ℝ E = finrank ℝ (ι → ℝ)<GOAL>ℝ≥0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>f' : α' → β'<VAR>q : Filter ι'<VAR>q' : Filter α'<VAR>h : TendstoUniformlyOnFilter F f p p'<VAR>h' : TendstoUniformlyOnFilter F' f' q q'<GOAL>TendstoUniformlyOnFilter (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>f' : α' → β'<VAR>q : Filter ι'<VAR>q' : Filter α'<VAR>h : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)<VAR>h' : Tendsto (fun q => (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')<GOAL>Tendsto (fun q => (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ((p ×ˢ q) ×ˢ p' ×ˢ q') (𝓤 (β × β'))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>f' : α' → β'<VAR>q : Filter ι'<VAR>q' : Filter α'<VAR>h : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)<VAR>h' : Tendsto (fun q => (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')<GOAL>Tendsto (((fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun q => (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((p ×ˢ p') ×ˢ q ×ˢ q') (𝓤 β ×ˢ 𝓤 β')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c : β<GOAL>c > fold max b f s ↔ b < c ∧ ∀ x ∈ s, f x < c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c : β<GOAL>∀ {x y z : β}, x > max y z ↔ x > y ∧ x > z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c x y z : β<GOAL>max y z < x ↔ x > y ∧ x > z
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝³ : Nonempty Z<VAR>inst✝² : MetricSpace Z<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>hΦ : Isometry Φ<VAR>hΨ : Isometry Ψ<VAR>i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ<VAR>x✝ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace<GOAL>toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝³ : Nonempty Z<VAR>inst✝² : MetricSpace Z<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>hΦ : Isometry Φ<VAR>hΨ : Isometry Ψ<VAR>i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ<VAR>x✝¹ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace<VAR>x✝ : Z<GOAL>(toGlueL hΦ hΨ ∘ Φ) x✝ = (toGlueR hΦ hΨ ∘ Ψ) x✝
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝³ : Nonempty Z<VAR>inst✝² : MetricSpace Z<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>hΦ : Isometry Φ<VAR>hΨ : Isometry Ψ<VAR>i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ<VAR>x✝¹ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace<VAR>x✝ : Z<GOAL>Quotient.mk'' (Sum.inl (Φ x✝)) = Quotient.mk'' (Sum.inr (Ψ x✝))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝³ : Nonempty Z<VAR>inst✝² : MetricSpace Z<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>hΦ : Isometry Φ<VAR>hΨ : Isometry Ψ<VAR>i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ<VAR>x✝¹ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace<VAR>x✝ : Z<GOAL>dist (Sum.inl (Φ x✝)) (Sum.inr (Ψ x✝)) = 0
<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>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<GOAL>(reflection s) (v +ᵥ p) = -v +ᵥ 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>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<GOAL>↑⟨p, hp⟩ -ᵥ p - v +ᵥ ↑⟨p, hp⟩ = -v +ᵥ p
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>K : Type u_5<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : Module K E<VAR>inst✝ : Module K F<VAR>f : E →ₗ.[K] F<VAR>x : E<VAR>y : F<VAR>hx : x ∉ f.domain<VAR>x' : E<VAR>hx' : x' ∈ f.domain<VAR>c : K<GOAL>↑(f.supSpanSingleton x y hx) ⟨x' + c • x, ⋯⟩ = ↑f ⟨x', hx'⟩ + c • y
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>K : Type u_5<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : Module K E<VAR>inst✝ : Module K F<VAR>f : E →ₗ.[K] F<VAR>x : E<VAR>y : F<VAR>hx : x ∉ f.domain<VAR>x' : E<VAR>hx' : x' ∈ f.domain<VAR>c : K<GOAL>c • x ∈ (mkSpanSingleton' x y ⋯).domain
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>K : Type u_5<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : Module K E<VAR>inst✝ : Module K F<VAR>f : E →ₗ.[K] F<VAR>x : E<VAR>y : F<VAR>hx : x ∉ f.domain<VAR>x' : E<VAR>hx' : x' ∈ f.domain<VAR>c : K<GOAL>↑⟨x', hx'⟩ + ↑⟨c • x, ?h⟩ = ↑⟨x' + c • x, ⋯⟩
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<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>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' G<VAR>inst✝ : SMulCommClass 𝕜 𝕜' G<GOAL>‖-f‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<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>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' G<VAR>inst✝ : SMulCommClass 𝕜 𝕜' G<GOAL>sInf {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖(-f) m‖ ≤ c * ∏ i : ι, ‖m i‖} = ‖f‖
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>g : G<VAR>K : Compacts G<GOAL>chaar K₀ (Compacts.map (fun b => g * b) ⋯ K) = chaar K₀ K
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>g : G<VAR>K : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K<GOAL>chaar K₀ (Compacts.map (fun b => g * b) ⋯ K) = chaar K₀ K
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>g : G<VAR>K : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K<VAR>this : Continuous eval<GOAL>chaar K₀ (Compacts.map (fun b => g * b) ⋯ K) = chaar K₀ K
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>g : G<VAR>K : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K<VAR>this : Continuous eval<GOAL>chaar K₀ (Compacts.map (fun b => g * b) ⋯ K) - chaar K₀ K = 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>g : G<VAR>K : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K<VAR>this : Continuous eval<GOAL>chaar K₀ ∈ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>g : G<VAR>K : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K<VAR>this : Continuous eval<GOAL>clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>g : G<VAR>K : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K<VAR>this : Continuous eval<GOAL>closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>g : G<VAR>K : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K<VAR>this : Continuous eval<GOAL>prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U} ⊆ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>g : G<VAR>K : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K<VAR>this : Continuous eval<GOAL>IsClosed (eval ⁻¹' {0})
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<GOAL>IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<GOAL>IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<VAR>a2 : InjOn (fun x => x ^ p) S<VAR>a3 : (fun t => t ^ p) '' S = S<GOAL>IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<VAR>a2 : InjOn (fun x => x ^ p) S<VAR>a3 : (fun t => t ^ p) '' S = S<VAR>this : IntegrableOn f ((fun t => t ^ p) '' Ioi 0) volume ↔ IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume<GOAL>IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<VAR>a2 : InjOn (fun x => x ^ p) S<VAR>a3 : (fun t => t ^ p) '' S = S<VAR>this : IntegrableOn f S volume ↔ IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume<GOAL>IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<VAR>a2 : InjOn (fun x => x ^ p) S<VAR>a3 : (fun t => t ^ p) '' S = S<VAR>this : IntegrableOn f S volume ↔ IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>(|p| * x ^ (p - 1)) • f (x ^ p) = |p * x ^ (p - 1)| • f (x ^ p)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s : Set ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint fun i' => (g i').sup f<VAR>hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f<VAR>a : ι<VAR>ha : a ∈ ⋃ i ∈ s, ↑(g i)<VAR>b : ι<VAR>hb : b ∈ ⋃ i ∈ s, ↑(g i)<VAR>hab : a ≠ b<GOAL>(Disjoint on f) a b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s : Set ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint fun i' => (g i').sup f<VAR>hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f<VAR>a b : ι<VAR>hab : a ≠ b<VAR>ha : ∃ i, ∃ (_ : i ∈ s), a ∈ ↑(g i)<VAR>hb : ∃ i, ∃ (_ : i ∈ s), b ∈ ↑(g i)<GOAL>(Disjoint on f) a b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s : Set ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint fun i' => (g i').sup f<VAR>hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f<VAR>a b : ι<VAR>hab : a ≠ b<VAR>c : ι'<VAR>hc : c ∈ s<VAR>ha : a ∈ ↑(g c)<VAR>d : ι'<VAR>hd : d ∈ s<VAR>hb : b ∈ ↑(g d)<GOAL>(Disjoint on f) a b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s : Set ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint fun i' => (g i').sup f<VAR>hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f<VAR>a b : ι<VAR>hab : a ≠ b<VAR>c : ι'<VAR>hc : c ∈ s<VAR>ha : a ∈ ↑(g c)<VAR>d : ι'<VAR>hd : d ∈ s<VAR>hb : b ∈ ↑(g d)<VAR>hcd : g c = g d<GOAL>(Disjoint on f) a b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s : Set ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint fun i' => (g i').sup f<VAR>hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f<VAR>a b : ι<VAR>hab : a ≠ b<VAR>c : ι'<VAR>hc : c ∈ s<VAR>ha : a ∈ ↑(g c)<VAR>d : ι'<VAR>hd : d ∈ s<VAR>hb : b ∈ ↑(g d)<VAR>hcd : g c ≠ g d<GOAL>(Disjoint on f) a b
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁✝ a₂ a₃ b b' b₁ b₂ b₃ c c₁ c₂ a₁ : R<VAR>x✝ : a₂ + b = c<GOAL>a₁ + a₂ + b = a₁ + c
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>s' : Set ((i : ι) → F' i)<VAR>id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)<GOAL>HasFDerivWithinAt (fun f => f i) (proj i) s' f
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>s' : Set ((i : ι) → F' i)<VAR>id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)<VAR>h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f<GOAL>HasFDerivWithinAt (fun f => f i) (proj i) s' f
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>s' : Set ((i : ι) → F' i)<VAR>id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)<VAR>h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f<VAR>h' : (proj i).comp id' = proj i<GOAL>HasFDerivWithinAt (fun f i' => f i') id' s' f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s ⊆ ⋂ i, ⋂ j, t i j ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝¹ : One α<VAR>inst✝ : TopologicalSpace X<VAR>f : X → α<GOAL>mulTSupport f = ∅ ↔ f = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>m : Fin n → 𝕜<GOAL>(iteratedFDerivWithin 𝕜 n f s x) m = (∏ i : Fin n, m i) • iteratedDerivWithin n f s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>m : Fin n → 𝕜<GOAL>(iteratedFDerivWithin 𝕜 n f s x) m = (iteratedFDerivWithin 𝕜 n f s x) fun i => m i • 1