ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 : 𝕜<GOAL>‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν✝ ν : Measure α<GOAL>rnDeriv 0 ν =ᶠ[ae ν] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν✝ ν : Measure α<GOAL>0 ⟂ₘ ν
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<GOAL>comap rexp (𝓝[>] 0) = atBot
<VAR>x : ℝ<GOAL>Real.toEReal '' Iic x = Ioc ⊥ ↑x
<VAR>x : ℝ<GOAL>WithBot.some '' (WithTop.some '' Iic x) = Ioc ⊥ ↑x
<VAR>x : ℝ<GOAL>Ioc ⊥ ↑↑x = Ioc ⊥ ↑x
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>x✝ : α<VAR>n : ℕ<GOAL>x✝ ∈ (a :: l).rotate (n + 1) ↔ x✝ ∈ a :: l
<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>x y : E<VAR>s t : Set E<VAR>a : ℝ<GOAL>(interior (Ici a)).Nonempty
<VAR>z : ℍ<GOAL>ModularGroup.S • z = mk (-↑z)⁻¹ ⋯
<VAR>z : ℍ<GOAL>mk ((↑((algebraMap ℤ ℝ) (↑↑ModularGroup.S 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑↑ModularGroup.S 0 1))) / (↑((algebraMap ℤ ℝ) (↑↑ModularGroup.S 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑↑ModularGroup.S 1 1)))) ⋯ = mk (-↑z)⁻¹ ⋯
<VAR>n : ℕ<GOAL>cos (↑n * (2 * π) + π) = -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>card { i // ↑i < m } = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>card { i // ↑i < m } = card (Fin m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>{ i // ↑i < m } ≃ Fin m
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : Semiring R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSemiring R<VAR>inst✝ : T2Space R<VAR>s : Set X<GOAL>IsClosed ↑(idealOfSet R s)
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : Semiring R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSemiring R<VAR>inst✝ : T2Space R<VAR>s : Set X<GOAL>IsClosed ↑{ carrier := ⋂ i ∈ sᶜ, {x | x i = 0}, add_mem' := ⋯, zero_mem' := ⋯ }
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>g : α → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)<GOAL>(μ.tilted f).rnDeriv ν =ᶠ[ae ν] fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>g : α → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)<GOAL>AEMeasurable g ν
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>g : α → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)<GOAL>∀ᵐ (x : α) ∂μ, g x ≠ ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<VAR>f_surj : Surjective f<VAR>ℱ : Filter Y<VAR>z : Z<VAR>h : MapClusterPt z ℱ g<GOAL>∃ x, g x = z ∧ ClusterPt x ℱ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<VAR>f_surj : Surjective f<VAR>ℱ : Filter Y<VAR>z : Z<VAR>h : MapClusterPt z (comap f ℱ) (g ∘ f)<GOAL>∃ x, g x = z ∧ ClusterPt x ℱ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<VAR>f_surj : Surjective f<VAR>ℱ : Filter Y<VAR>x : X<VAR>hx : ClusterPt x (comap f ℱ)<VAR>h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)<GOAL>∃ x_1, g x_1 = (g ∘ f) x ∧ ClusterPt x_1 ℱ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<VAR>f_surj : Surjective f<VAR>ℱ : Filter Y<VAR>x : X<VAR>hx : ClusterPt x (comap f ℱ)<VAR>h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)<GOAL>∃ x_1, g x_1 = (g ∘ f) x ∧ ClusterPt x_1 (map f (comap f ℱ))
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>I✝ : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>I : Type u_2<VAR>c : R<VAR>x✝ : I<GOAL>(↑↑{ toFun := fun h => ⇑f ∘ h, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }).toFun ((algebraMap R (I → A)) c) x✝ = (algebraMap R (I → B)) c x✝
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra 𝕜 A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : NormOneClass A<VAR>a : A<VAR>k : 𝕜<VAR>hk : k ∈ σ a<GOAL>k ∈ Metric.closedBall 0 ‖a‖
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>s t : Set P1<VAR>f : P1 →ᵃ[k] P2<VAR>v : V2<GOAL>v ∈ ⇑f '' s -ᵥ ⇑f '' t ↔ v ∈ ⇑f.linear '' (s -ᵥ t)
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>s t : Set P1<VAR>f : P1 →ᵃ[k] P2<VAR>v : V2<GOAL>(∃ a ∈ s, ∃ a_1 ∈ t, f.linear (a -ᵥ a_1) = v) ↔ ∃ x, (∃ x_1 ∈ s, ∃ y ∈ t, x_1 -ᵥ y = x) ∧ f.linear x = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<VAR>f : α → β<GOAL>ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a
<VAR>n✝ p n : ℕ<GOAL>(p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
<VAR>n✝ p n : ℕ<VAR>h : 1 < p<GOAL>(p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
<VAR>n✝ n : ℕ<GOAL>(1 - 1) * ∑ i ∈ range (log 1 n).succ, n / 1 ^ i.succ = n - (digits 1 n).sum
<VAR>n✝ p n : ℕ<VAR>h : p < 1<GOAL>(p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>x : R<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i : m<VAR>j✝ : n<VAR>b : n → α<VAR>c✝ : m → α<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : DecidableEq n<VAR>A : Matrix m n α<VAR>j : o<VAR>c : l → α<VAR>e : l ≃ m<VAR>f : o ≃ n<GOAL>(A.submatrix ⇑e ⇑f).updateColumn j c = (A.updateColumn (f j) fun i => c (e.symm i)).submatrix ⇑e ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>H : IsNormal f<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<VAR>a : Ordinal.{u_5}<GOAL>¬a < f o ↔ ¬∃ b < o, a < f b
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<GOAL>(lookupAll a l).Nodup
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<VAR>n : ℕ<GOAL>((monomial n) r * p).smeval x = r • (x ^ n * p.smeval x)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>a b y : α<VAR>hya : y ∈ Ici a<VAR>z : α<VAR>hzb : z ∈ Ici b<GOAL>(fun x x_1 => x * x_1) y z ∈ Ici (a * b)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f✝ : (i : ι) → s i →ₗ[R] t i<VAR>f : (i : ι) → s i ≃ₗ[R] t i<VAR>p : (i : ι) → t i<GOAL>(congr f).symm ((tprod R) p) = ⨂ₜ[R] (i : ι), (f i).symm (p i)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<GOAL>Iic a * Iio b ⊆ Iio (a * b)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<VAR>this : ∀ (M : Type ?u.9430) (N : Type ?u.9429) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<GOAL>Iic a * Iio b ⊆ Iio (a * b)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<VAR>this : ∀ (M : Type ?u.9430) (N : Type ?u.9429) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>y : α<VAR>hya : y ∈ Iic a<VAR>z : α<VAR>hzb : z ∈ Iio b<GOAL>(fun x x_1 => x * x_1) y z ∈ Iio (a * b)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ p₄ p₅ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₄, p₅}<VAR>h₂ : p₂ ∈ affineSpan k {p₄, p₅}<VAR>h₃ : p₃ ∈ affineSpan k {p₄, p₅}<GOAL>Collinear k {p₁, p₂, p₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ p₄ p₅ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₄, p₅}<VAR>h₂ : p₂ ∈ affineSpan k {p₄, p₅}<VAR>h₃ : p₃ ∈ affineSpan k {p₄, p₅}<GOAL>{p₁, p₂, p₃} ⊆ {p₁, p₂, p₃, p₄}
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P : Cᵒᵖ ⥤ D<VAR>hP : Presheaf.IsSheaf J P<GOAL>(isoSheafify J hP).inv = sheafifyLift J (𝟙 P) hP
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P : Cᵒᵖ ⥤ D<VAR>hP : Presheaf.IsSheaf J P<GOAL>toSheafify J P ≫ (isoSheafify J hP).inv = 𝟙 P
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<GOAL>topologicalSpace α β 𝔖 = ⨅ s ∈ 𝔖, TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.topologicalSpace (↑s) β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<GOAL>⨅ i ∈ 𝔖, UniformSpace.toTopologicalSpace = ⨅ s ∈ 𝔖, TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.topologicalSpace (↑s) β)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<GOAL>(X ^ n).degree ≤ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MulOneClass α<VAR>inst✝¹ : LT α<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : b < a * b<GOAL>1 * b < a * b
<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>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<VAR>x : E<GOAL>↑((p.linearProjOfIsCompl (ker f) ⋯) x) = ↑(f x)
<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>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<VAR>x : E<VAR>this : x ∈ p ⊔ ker f<GOAL>↑((p.linearProjOfIsCompl (ker f) ⋯) x) = ↑(f x)
<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>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<VAR>x : ↥p<VAR>y : ↥(ker f)<VAR>this : ↑x + ↑y ∈ p ⊔ ker f<GOAL>↑((p.linearProjOfIsCompl (ker f) ⋯) (↑x + ↑y)) = ↑(f (↑x + ↑y))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Zero α<VAR>v : l ⊕ m → α<GOAL>(of fun i j => diagonal v (Sum.inr i) (Sum.inr j)) = diagonal fun i => v (Sum.inr i)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Zero α<VAR>v : l ⊕ m → α<VAR>i j : m<GOAL>of (fun i j => diagonal v (Sum.inr i) (Sum.inr j)) i j = diagonal (fun i => v (Sum.inr i)) i j
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<GOAL>Tendsto (fun n => setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<GOAL>Tendsto (fun n => setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<GOAL>Tendsto (fun n => setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<GOAL>Tendsto (fun n => setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<GOAL>Tendsto (fun n => (L1.setToL1 hT) (Integrable.toL1 (fs n) ⋯)) atTop (𝓝 ((L1.setToL1 hT) (Integrable.toL1 f f_int)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<GOAL>Tendsto (fun n => Integrable.toL1 (fs n) ⋯) atTop (𝓝 (Integrable.toL1 f f_int))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<GOAL>Tendsto (fun e => ‖Integrable.toL1 (fs e) ⋯ - Integrable.toL1 f f_int‖) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<VAR>lintegral_norm_tendsto_zero : Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)<GOAL>Tendsto (fun e => ‖Integrable.toL1 (fs e) ⋯ - Integrable.toL1 f f_int‖) atTop (𝓝 0)