ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>s : Set M<VAR>hs : IsOpen s<GOAL>∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>s : Set M<VAR>hs : IsOpen s<VAR>f : SmoothPartitionOfUnity M I M<VAR>hf : f.IsSubordinate fun x => (chartAt H x).source<GOAL>∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>s : Set M<VAR>hs : IsOpen s<VAR>f : SmoothPartitionOfUnity M I M<VAR>hf : f.IsSubordinate fun x => (chartAt H x).source<VAR>A : ∀ (c : M), ∃ g, support g = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s ∧ Smooth I 𝓘(ℝ, ℝ) g ∧ range g ⊆ Icc 0 1<GOAL>∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>s : Set M<VAR>hs : IsOpen s<VAR>f : SmoothPartitionOfUnity M I M<VAR>hf : f.IsSubordinate fun x => (chartAt H x).source<VAR>g : M → H → ℝ<VAR>g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s<VAR>g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)<VAR>hg : ∀ (c : M), range (g c) ⊆ Icc 0 1<GOAL>∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>s : Set M<VAR>hs : IsOpen s<VAR>f : SmoothPartitionOfUnity M I M<VAR>hf : f.IsSubordinate fun x => (chartAt H x).source<VAR>g : M → H → ℝ<VAR>g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s<VAR>g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)<VAR>hg : ∀ (c : M), range (g c) ⊆ Icc 0 1<VAR>h'g : ∀ (c : M) (x : H), 0 ≤ g c x<GOAL>∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>s : Set M<VAR>hs : IsOpen s<VAR>f : SmoothPartitionOfUnity M I M<VAR>hf : f.IsSubordinate fun x => (chartAt H x).source<VAR>g : M → H → ℝ<VAR>g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s<VAR>g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)<VAR>hg : ∀ (c : M), range (g c) ⊆ Icc 0 1<VAR>h'g : ∀ (c : M) (x : H), 0 ≤ g c x<VAR>h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)<GOAL>∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>r : R<GOAL>star ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n : ℕ<VAR>ha : a ∈ s<GOAL>a ^ 0 ∈ s ^ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n : ℕ<VAR>ha : a ∈ s<GOAL>1 ∈ s ^ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n✝ : ℕ<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>a ^ (n + 1) ∈ s ^ (n + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n✝ : ℕ<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>a ^ n * a ∈ s ^ (n + 1)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsAffine X<VAR>inst✝ : IsAffine Y<GOAL>P f ↔ Q (Scheme.Hom.app f ⊤)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsAffine X<VAR>inst✝ : IsAffine Y<GOAL>(∀ (i : (Scheme.openCoverOfIsIso (𝟙 X)).J), Q (Scheme.Hom.app ((Scheme.openCoverOfIsIso (𝟙 X)).map i ≫ f) ⊤)) ↔ Q (Scheme.Hom.app f ⊤)
<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>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>(o.oangle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ + -1 • (p₃ -ᵥ p₂))).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
<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>(o.oangle (p₁ -ᵥ p₂) (1 • (p₁ -ᵥ p₂) + -1 • (p₃ -ᵥ p₂))).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
<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>SignType.sign (-1) * (o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidablePred fun x => b ≤ x<GOAL>filter (fun x => b ≤ x) (Ico a b) = ∅
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidablePred fun x => b ≤ x<GOAL>∅.val = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : AddGroupWithOne R<GOAL>↑(s ∩ t).card = ↑s.card + ↑t.card - ↑(s ∪ t).card
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁷ : Category.{?u.218597, u_1} C₁<VAR>inst✝⁶ : Category.{?u.218601, u_2} C₂<VAR>inst✝⁵ : Category.{?u.218605, u_3} C₃<VAR>inst✝⁴ : Category.{?u.218609, u_4} C₄<VAR>inst✝³ : Category.{?u.218613, u_5} C₁₂<VAR>inst✝² : Category.{?u.218617, u_6} C₂₃<VAR>F✝ F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₂₃ : BifunctorComp₂₃IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<VAR>i₂₃ : ρ₂₃.I₂₃<VAR>h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃<GOAL>ρ₂₃.q (i₁, i₂₃) = j
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)<VAR>this : TopologicalAddGroup F<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)<VAR>this : TopologicalAddGroup F<GOAL>ContinuousAt (⇑f) 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)<VAR>this : TopologicalAddGroup F<GOAL>∀ (i : ι'), Tendsto (⇑(q i) ∘ ⇑f) (𝓝 0) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)<VAR>this : TopologicalAddGroup F<VAR>i : ι'<GOAL>Tendsto (⇑(q i) ∘ ⇑f) (𝓝 0) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)<VAR>this : TopologicalAddGroup F<VAR>i : ι'<GOAL>0 = ((q i).comp f) 0
<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>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>x : G<VAR>f' : G →L[𝕜] F<GOAL>HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f ((↑iso.symm).comp f') x
<VAR>n : ℕ<VAR>h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2<VAR>h2 : fib (n.succ + 1) = ∑ p ∈ Finset.antidiagonal n.succ, p.1.choose p.2<GOAL>fib (n.succ.succ + 1) = ∑ p ∈ Finset.antidiagonal n.succ.succ, p.1.choose p.2
<VAR>n : ℕ<VAR>h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2<VAR>h2 : fib (n.succ + 1) = ∑ p ∈ Finset.antidiagonal n.succ, p.1.choose p.2<GOAL>∑ p ∈ Finset.antidiagonal n, p.1.choose p.2 + ∑ p ∈ Finset.cons (n + 1, 0) (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := succ, inj' := succ_injective }) (Finset.antidiagonal n)) ⋯, p.1.choose p.2 = ∑ p ∈ Finset.cons (0, n + 2) (Finset.cons (n + 2, 0) (Finset.map ({ toFun := succ, inj' := succ_injective }.prodMap { toFun := succ, inj' := succ_injective }) (Finset.antidiagonal n)) ⋯) ⋯, p.1.choose p.2
<VAR>R : Type u<VAR>S : Type v<VAR>a b✝ : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>b : R<VAR>hp : b * p.leadingCoeff = 1<VAR>a✝ : Nontrivial R<GOAL>(C b * p).leadingCoeff = 1
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<VAR>v : Set α := u ∩ V<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<VAR>v : Set α := u ∩ V<VAR>hsv : s ⊆ v<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<VAR>v : Set α := u ∩ V<VAR>hsv : s ⊆ v<VAR>hμv : μ v < ⊤<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<VAR>v : Set α := u ∩ V<VAR>hsv : s ⊆ v<VAR>hμv : μ v < ⊤<VAR>g : C(α, ℝ)<VAR>hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ<VAR>hgs : EqOn (⇑g) 1 s<VAR>hg_range : ∀ (x : α), g x ∈ Icc 0 1<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>η : ℝ≥0<VAR>η_pos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε<VAR>ηpos : 0 < ↑η<VAR>V : Set α<VAR>sV : V ⊇ s<VAR>V_open : IsOpen V<VAR>h'V : μ V < ⊤<VAR>hV : μ (V \ s) < ↑η<VAR>v : Set α := u ∩ V<VAR>hsv : s ⊆ v<VAR>hμv : μ v < ⊤<VAR>g : C(α, ℝ)<VAR>hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ<VAR>hgs : EqOn (⇑g) 1 s<VAR>hg_range : ∀ (x : α), g x ∈ Icc 0 1<VAR>g_norm : ∀ (x : α), ‖g x‖ = g x<GOAL>∃ f, Continuous f ∧ eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p μ