ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<GOAL>(ν a) univ ^ (ENNReal.toReal 1)⁻¹ * ENNReal.ofReal 1 ≤ (ν a) univ
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>a : α<VAR>b : β<VAR>l : List (α × β)<GOAL>((a, b) :: l).unzip = (map Prod.fst ((a, b) :: l), map Prod.snd ((a, b) :: l))
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>x y z : L<GOAL>(__spread✝⁻⁰.toFun ⁅x, y⁆) z = ⁅__spread✝⁻⁰.toFun x, __spread✝⁻⁰.toFun y⁆ z
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>x y z : L<GOAL>-⁅z, ⁅x, y⁆⁆ = -⁅-⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>x y z : L<GOAL>-(⁅⁅z, x⁆, y⁆ + -⁅⁅z, y⁆, x⁆) = - -⁅⁅z, y⁆, x⁆ - - -⁅⁅z, x⁆, y⁆
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝² : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>hN : {i | N i ≠ ⊥}.Finite<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)<VAR>x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype<VAR>x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype<GOAL>(trace R M) f = ∑ i ∈ hN.toFinset, (trace R ↥(N i)) (f.restrict ⋯)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝² : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>hN : {i | N i ≠ ⊥}.Finite<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)<VAR>x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype<VAR>x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype<GOAL>∑ i : { i // N i ≠ ⊥ }, (trace R ↥(N ↑i)) (f.restrict ⋯) = ∑ i : { x // x ∈ hN.toFinset }, (trace R ↥(N ↑i)) (f.restrict ⋯)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝² : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>hN : {i | N i ≠ ⊥}.Finite<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)<VAR>x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype<VAR>x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype<GOAL>∀ (i : { i // N i ≠ ⊥ }), MapsTo ⇑f ↑(N ↑i) ↑(N ↑i)
<VAR>z : ℍ<GOAL>0 < (-↑z)⁻¹.im
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : β → α<VAR>p : β → Prop<GOAL>⨆ i, f i = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), f i
<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 α)<VAR>hs : s ∈ 𝔖<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<GOAL>UniformOnFun.gen 𝔖 s V ∈ 𝓤 (α →ᵤ[𝔖] β)
<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 α)<VAR>hs : s ∈ 𝔖<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<GOAL>UniformOnFun.gen 𝔖 s V ∈ ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : StrictOrderedSemiring R<VAR>a x y : R<VAR>n m : ℕ<VAR>h : 1 < a<VAR>hm : 1 < m<GOAL>a < a ^ m
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<GOAL>Convex 𝕜 s ↔ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<GOAL>(s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s<VAR>x : E<VAR>hx : x ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hy : x ∈ s<GOAL>a • x + b • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hxy : x ≠ y<GOAL>a • x + b • y ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a : α<VAR>hb : Sum.inl b ∈ f a<GOAL>b ∈ f.fix a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a : α<VAR>hb : Sum.inl b ∈ f a<GOAL>Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : ↑(map f I) = ⇑f '' ↑I<GOAL>comap f (map f I) = I ⊔ f.ker
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>Summable (f_int k a t)
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>Summable fun a_1 => ‖f_int k a t a_1‖
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>∀ (n : ℤ), ‖f_int k a t n‖ = ‖(fun t_1 => Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) n‖
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.7462, u_1} C<VAR>Φ : C ⥤ C<VAR>ε : 𝟭 C ⟶ Φ<VAR>J : Type u<VAR>inst✝² : LinearOrder J<VAR>inst✝¹ : IsWellOrder J fun x x_1 => x < x_1<VAR>inst✝ : OrderBot J<VAR>j : J<VAR>F : { i // i ≤ j } ⥤ C<VAR>i : J<VAR>hi : i ≤ j<VAR>k₁ k₂ : { k // k < i }<VAR>φ : k₁ ⟶ k₂<GOAL>⋯.functor.obj k₁ ≤ ⋯.functor.obj k₂
<VAR>n : ℕ<GOAL>0 < powHalf n
<VAR>n : ℕ<GOAL>∃ i, 0 ≤ (powHalf n).moveLeft i
<VAR>α✝ : Sort u<VAR>β✝ : α✝ → Sort v<VAR>α' : Sort w<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : DecidableEq α'<VAR>f✝ g : (a : α✝) → β✝ a<VAR>a✝ : α✝<VAR>b : β✝ a✝<VAR>α : Sort u_2<VAR>inst✝ : DecidableEq α<VAR>β : α → Sort u_1<VAR>a : α<VAR>v w : β a<VAR>f : (a : α) → β a<GOAL>update (update f a v) a w = update f a w
<VAR>α✝ : Sort u<VAR>β✝ : α✝ → Sort v<VAR>α' : Sort w<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : DecidableEq α'<VAR>f✝ g : (a : α✝) → β✝ a<VAR>a✝ : α✝<VAR>b✝ : β✝ a✝<VAR>α : Sort u_2<VAR>inst✝ : DecidableEq α<VAR>β : α → Sort u_1<VAR>a : α<VAR>v w : β a<VAR>f : (a : α) → β a<VAR>b : α<GOAL>update (update f a v) a w b = update f a w b
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>F✝ G H : A ⥤ B<VAR>η : F✝ ⟶ G<VAR>γ : G ⟶ H<VAR>inst✝⁴ : J.HasSheafCompose F✝<VAR>inst✝³ : J.HasSheafCompose G<VAR>inst✝² : J.HasSheafCompose H<VAR>inst✝¹ : ConcreteCategory A<VAR>inst✝ : J.HasSheafCompose (forget A)<VAR>F : Sheaf J A<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<VAR>x y : (forget A).obj (F.val.obj (Opposite.op X))<VAR>h : ∀ (Y : C) (f : Y ⟶ X), S.arrows f → (F.val.map f.op) x = (F.val.map f.op) y<GOAL>x = y
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hx : ‖x‖ < r<GOAL>Absorbent 𝕜 (Metric.ball x r)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hx : ‖x‖ < r<GOAL>Absorbent 𝕜 ((normSeminorm 𝕜 E).ball x r)
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>a b c d : α<VAR>h : a < b<GOAL>𝓝ˢ (Ioc a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
<VAR>E : Type u_1<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>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>￢(a ⊓ b) = ￢a ⊔ ￢b
<VAR>θ : Angle<GOAL>θ = -θ ↔ θ = 0 ∨ θ = ↑π
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>count p (n + 1) = count p n + 1 ↔ p n
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>BfactorSetMem ⟨p, hp⟩ ⊤
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{max u v}<GOAL>sum f ≤ lift.{v, u} #ι * iSup f
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{max u v}<GOAL>sum f ≤ sum fun x => iSup f
<VAR>a b c : ℕ<VAR>h : c ≤ a<VAR>x : ℕ<GOAL>x ∈ image (fun x => x - c) (Ico a b) ↔ x ∈ Ico (a - c) (b - c)
<VAR>a b c : ℕ<VAR>h : c ≤ a<VAR>x : ℕ<GOAL>(∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) ↔ a - c ≤ x ∧ x < b - c
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hL : f₁ =ᶠ[𝓝 x] f<GOAL>mfderiv I I' f₁ x = mfderiv I I' f x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hL : f₁ =ᶠ[𝓝 x] f<VAR>A : f₁ x = f x<GOAL>mfderiv I I' f₁ x = mfderiv I I' f x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hL : f₁ =ᶠ[𝓝 x] f<VAR>A : f₁ x = f x<GOAL>mfderivWithin I I' f₁ univ x = mfderivWithin I I' f univ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hL : f₁ =ᶠ[𝓝[univ] x] f<VAR>A : f₁ x = f x<GOAL>mfderivWithin I I' f₁ univ x = mfderivWithin I I' f univ x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ : F ⟶ G<VAR>p q q' : ℤ<VAR>hpq : p + 0 = q<GOAL>(ofHom φ).v p q hpq ≫ G.d q q' = φ.f p ≫ G.d p q'
<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>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>D : ℝ := max C 1<GOAL>Continuous ⇑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>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>D : ℝ := max C 1<VAR>D_pos : 0 ≤ D<GOAL>Continuous ⇑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>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>D : ℝ := max C 1<VAR>D_pos : 0 ≤ D<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i : ι, ‖m i‖<GOAL>Continuous ⇑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>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>D : ℝ := max C 1<VAR>D_pos : 0 ≤ D<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i : ι, ‖m i‖<VAR>m : (i : ι) → E i<GOAL>ContinuousAt (⇑f) m
<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>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>D : ℝ := max C 1<VAR>D_pos : 0 ≤ D<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i : ι, ‖m i‖<VAR>m m' : (i : ι) → E i<VAR>h' : dist m' m < 1<GOAL>dist (f m') (f m) ≤ D * ↑(Fintype.card ι) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * dist m' m
<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>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>D : ℝ := max C 1<VAR>D_pos : 0 ≤ D<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i : ι, ‖m i‖<VAR>m m' : (i : ι) → E i<VAR>h' : dist m' m < 1<GOAL>‖f m' - f m‖ ≤ D * ↑(Fintype.card ι) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖
<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>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>D : ℝ := max C 1<VAR>D_pos : 0 ≤ D<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i : ι, ‖m i‖<VAR>m m' : (i : ι) → E i<VAR>h' : dist m' m < 1<VAR>this : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1<GOAL>‖f m' - f m‖ ≤ D * ↑(Fintype.card ι) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<GOAL>∫ (b : β), ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a = ((κ a) (univ ×ˢ Iic x)).toReal
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>η✝ : 𝟙 a ≅ f ≫ g<VAR>ε✝ : g ≫ f ≅ 𝟙 b<VAR>η : 𝟙 a ≅ f ≫ g<VAR>ε : g ≫ f ≅ 𝟙 b<GOAL>leftZigzagIso η (adjointifyCounit η ε) = λ_ f ≪≫ (ρ_ f).symm
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>η✝ : 𝟙 a ≅ f ≫ g<VAR>ε✝ : g ≫ f ≅ 𝟙 b<VAR>η : 𝟙 a ≅ f ≫ g<VAR>ε : g ≫ f ≅ 𝟙 b<GOAL>(leftZigzagIso η (adjointifyCounit η ε)).hom = (λ_ f ≪≫ (ρ_ f).symm).hom
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>η✝ : 𝟙 a ≅ f ≫ g<VAR>ε✝ : g ≫ f ≅ 𝟙 b<VAR>η : 𝟙 a ≅ f ≫ g<VAR>ε : g ≫ f ≅ 𝟙 b<GOAL>η.hom ▷ f ≫ ((α_ f g f).hom ≫ 𝟙 f ▷ (g ≫ f)) ≫ f ◁ (g ◁ ((ρ_ f).inv ≫ (f ◁ ε.inv ≫ (𝟙 f ▷ (g ≫ f) ≫ (α_ f g f).inv) ≫ η.inv ▷ f) ≫ (λ_ f).hom) ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))