ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>a : Set α<VAR>h'a : μ a < ⊤<VAR>h''a : IntegrableOn f a μ<GOAL>(ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) a = ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>a : Set α<VAR>h'a : μ a < ⊤<VAR>h''a : IntegrableOn f a μ<GOAL>(μ a).toReal⁻¹ * (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ).toReal = (μ a).toReal⁻¹ • ∫ (y : α) in a, ‖f y - f x‖ ∂μ
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>a : Set α<VAR>h'a : μ a < ⊤<VAR>h''a : IntegrableOn f a μ<VAR>A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a μ<GOAL>(μ a).toReal⁻¹ * (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ).toReal = (μ a).toReal⁻¹ • ∫ (y : α) in a, ‖f y - f x‖ ∂μ
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>a : Set α<VAR>h'a : μ a < ⊤<VAR>h''a : IntegrableOn f a μ<VAR>A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a μ<GOAL>(μ a).toReal⁻¹ * ∫ (a : α) in a, ↑‖f a - f x‖₊ ∂μ = (μ a).toReal⁻¹ • ∫ (y : α) in a, ‖f y - f x‖ ∂μ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n✝ : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>a : R<VAR>n : σ →₀ ℕ<GOAL>Commute φ ((monomial R n) a) ↔ ∀ (m : σ →₀ ℕ), Commute ((coeff R m) φ) a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m✝ n✝ : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>a : R<VAR>n : σ →₀ ℕ<VAR>h : ∀ (n_1 : σ →₀ ℕ), (coeff R n_1) (φ * (monomial R n) a) = (coeff R n_1) ((monomial R n) a * φ)<VAR>m : σ →₀ ℕ<GOAL>Commute ((coeff R m) φ) a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m✝ n✝ : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>a : R<VAR>n : σ →₀ ℕ<VAR>h : ∀ (m : σ →₀ ℕ), Commute ((coeff R m) φ) a<VAR>m : σ →₀ ℕ<GOAL>(coeff R m) (φ * (monomial R n) a) = (coeff R m) ((monomial R n) a * φ)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>n : ℕ<GOAL>‖↑n‖ = ↑n
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>n : ℕ<GOAL>‖↑↑n‖ = ↑n
<VAR>R✝ : Type u<VAR>S : Type v<VAR>a✝ b : R✝<VAR>m n✝ : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Ring R✝<VAR>p : R✝[X]<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>a : R<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(X ^ n - C a).Monic
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>h : ∀ a < type r, succ a < type r<VAR>x : α<GOAL>∃ y, r x y
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>h : ∀ a < type r, succ a < type r<VAR>x : α<GOAL>r x (enum r (succ (typein r x)) ⋯)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>h : ∀ a < type r, succ a < type r<VAR>x : α<GOAL>x = enum r (typein r x) ⋯
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>h : IsCyclic G<VAR>σ : G →* G<GOAL>∃ m, ∀ (g : G), σ g = g ^ m
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>h✝ : IsCyclic G<VAR>σ : G →* G<VAR>h : G<VAR>hG : ∀ (x : G), x ∈ zpowers h<GOAL>∃ m, ∀ (g : G), σ g = g ^ m
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>h✝ : IsCyclic G<VAR>σ : G →* G<VAR>h : G<VAR>hG : ∀ (x : G), x ∈ zpowers h<VAR>m : ℤ<VAR>hm : (fun x => h ^ x) m = σ h<VAR>n : ℤ<GOAL>σ ((fun x => h ^ x) n) = (fun x => h ^ x) n ^ m
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : T2Space γ<VAR>inst✝ : CompactSpace γ<VAR>f : α → γ<GOAL>Continuous (Ultrafilter.extend f)
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : T2Space γ<VAR>inst✝ : CompactSpace γ<VAR>f : α → γ<VAR>h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)<GOAL>Continuous (Ultrafilter.extend f)
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : T2Space γ<VAR>inst✝ : CompactSpace γ<VAR>f : α → γ<VAR>h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)<VAR>x✝ : TopologicalSpace α := ⊥<GOAL>Continuous (Ultrafilter.extend f)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<GOAL>TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
<VAR>a b : ℝ<VAR>h : b ≠ 0<GOAL>ContinuousAt (fun x => a ^ x) b
<VAR>a b : ℝ<VAR>h : b ≠ 0<GOAL>ContinuousAt (fun x => (↑a ^ ↑x).re) b
<VAR>a b : ℝ<VAR>h : b ≠ 0<GOAL>ContinuousAt (fun x => ↑a ^ ↑x) b
<VAR>a b : ℝ<VAR>h : b ≠ 0<GOAL>↑b ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLinearOrder α<VAR>s : Set α<VAR>f : ι → α<VAR>x : α<VAR>hlim : ¬IsSuccLimit (sSup s)<GOAL>sSup s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLinearOrder α<VAR>s : Set α<VAR>f : ι → α<VAR>x : α<VAR>hlim : ¬IsSuccLimit (sSup s)<VAR>y : α<VAR>hy : y ⋖ sSup s<GOAL>sSup s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLinearOrder α<VAR>s : Set α<VAR>f : ι → α<VAR>x : α<VAR>hlim : ¬IsSuccLimit (sSup s)<VAR>y : α<VAR>hy : y ⋖ sSup s<VAR>i : α<VAR>his : i ∈ s<VAR>hi : y < i<GOAL>sSup s ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>s : Finset α<VAR>f : α → M<VAR>hf : ∀ (a : α), f a ≠ 0 → a ∈ s<VAR>a : α<GOAL>a ∈ (onFinset s f hf).support ↔ f a ≠ 0
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A⁻¹.det * A.det = 1
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapb : ∠ a p b = π<VAR>hcpd : ∠ c p d = π<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapb : ∠ a p b = π<VAR>hcpd : ∠ c p d = π<VAR>k₁ : ℝ<VAR>left✝ : k₁ < 0<VAR>hab : b -ᵥ p = k₁ • (a -ᵥ p)<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapb : ∠ a p b = π<VAR>hcpd : ∠ c p d = π<VAR>k₁ : ℝ<VAR>left✝¹ : k₁ < 0<VAR>hab : b -ᵥ p = k₁ • (a -ᵥ p)<VAR>k₂ : ℝ<VAR>left✝ : k₂ < 0<VAR>hcd : d -ᵥ p = k₂ • (c -ᵥ p)<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.284157, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting<VAR>inst✝ : HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>n : ℤ<GOAL>(snd φ).v n n ⋯ ≫ ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)).f + ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)).g ≫ (-(inl φ).v (n + 1) n ⋯) = 𝟙 ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)).X₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>(adjoin.powerBasis' hx).gen = ⟨x, ⋯⟩
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m n m' : M<VAR>f : m ⟶ m'<VAR>X : C<GOAL>(F.μIso m n).inv.app X ≫ (F.obj n).map ((F.map f).app X) = (F.map (f ▷ n)).app X ≫ (F.μIso m' n).inv.app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m n m' : M<VAR>f : m ⟶ m'<VAR>X : C<GOAL>(F.obj n).map ((F.map f).app X) ≫ inv ((F.μIso m' n).inv.app X) = inv ((F.μIso m n).inv.app X) ≫ (F.map (f ▷ n)).app X
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime y (z * x) ↔ IsRelPrime y z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<GOAL>IsExtreme 𝕜 A {x} ↔ x ∈ extremePoints 𝕜 A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<GOAL>x ∈ extremePoints 𝕜 A → IsExtreme 𝕜 A {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<VAR>hxA : x ∈ A<VAR>hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x<GOAL>IsExtreme 𝕜 A {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<VAR>hxA : x ∈ A<VAR>hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x<GOAL>∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → ∀ ⦃x_1 : E⦄, x_1 ∈ {x} → x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ {x} ∧ x₂ ∈ {x}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ✝ μ : Measure α<VAR>x✝¹ : Set α<VAR>x✝ : MeasurableSet x✝¹<VAR>h0 : μ x✝¹ ≠ 0<GOAL>∃ x ∈ x✝¹, ∃ m, m ≠ 0 ∧ id^[m] x ∈ x✝¹
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>c : F<GOAL>HasDerivAtFilter (fun x => f x - c) f' x L
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<GOAL>𝓝 ⊤ = ⊤
<VAR>α : Type u_1<VAR>s t : Set α<VAR>x : α × α<VAR>a : α<VAR>ha : a ∉ s<GOAL>(insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}
<VAR>α : Type u_1<VAR>s t : Set α<VAR>x : α × α<VAR>a : α<VAR>ha : a ∉ s<GOAL>Disjoint s {a}
<VAR>α : Type u_1<VAR>s t : Set α<VAR>x : α × α<VAR>a : α<VAR>ha : a ∉ s<GOAL>∀ ⦃a_1 : α⦄, a_1 ∈ s → a_1 ∉ {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>Ixx : α → α → Set α<GOAL>Tendsto (fun p => Ixx p.1 p.2) (𝓟 s ×ˢ 𝓟 s) (𝓟 t).smallSets ↔ ∀ x ∈ s, ∀ y ∈ s, Ixx x y ⊆ t
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>k : α<VAR>n : ℤ<VAR>x a a' : α<VAR>h : k + a = a'<GOAL>k + termg n x a = termg n x a'
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>0 < ∫ (x : ℝ) in 0 ..π, sin x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hf : ∀ (i : α), ContDiff 𝕜 N (f i)<VAR>hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)<VAR>h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i<GOAL>ContDiff 𝕜 N fun x => ∑' (i : α), f i x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hf : ∀ (i : α), ContDiff 𝕜 N (f i)<VAR>hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)<VAR>h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i<GOAL>(∀ (m : ℕ), ↑m ≤ N → Continuous fun x => iteratedFDeriv 𝕜 m (fun x => ∑' (i : α), f i x) x) ∧ ∀ (m : ℕ), ↑m < N → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m (fun x => ∑' (i : α), f i x) x
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : StrongRankCondition R<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Free R M'<VAR>m : Type v<VAR>n : Type w<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<GOAL>Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : StrongRankCondition R<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Free R M'<VAR>m : Type v<VAR>n : Type w<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<VAR>val✝ : Fintype m<GOAL>Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : StrongRankCondition R<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Free R M'<VAR>m : Type v<VAR>n : Type w<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<VAR>val✝¹ : Fintype m<VAR>val✝ : Fintype n<GOAL>Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : StrongRankCondition R<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Free R M'<VAR>m : Type v<VAR>n : Type w<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<VAR>val✝¹ : Fintype m<VAR>val✝ : Fintype n<VAR>h : lift.{max (max u v) w, max v w} #(m × n) = lift.{max v w, max (max u v) w} (Module.rank R (Matrix m n R))<GOAL>Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : StrongRankCondition R<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Free R M'<VAR>m : Type v<VAR>n : Type w<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<VAR>val✝¹ : Fintype m<VAR>val✝ : Fintype n<VAR>h : lift.{max v w u, max v w} #(m × n) = Module.rank R (Matrix m n R)<GOAL>Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f : E → ℝ<GOAL>StrongConcaveOn s m f ↔ ConcaveOn ℝ s fun x => f x + m / 2 * ‖x‖ ^ 2
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝³ y✝ : E<VAR>f : E → ℝ<VAR>x✝² : Convex ℝ s<VAR>x : E<VAR>x✝¹ : x ∈ s<VAR>y : E<VAR>x✝ : y ∈ s<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y + a * b * (fun r => m / 2 * r ^ 2) ‖x - y‖ ≤ f (a • x + b • y) ↔ a • (fun x => f x + m / 2 * ‖x‖ ^ 2) x + b • (fun x => f x + m / 2 * ‖x‖ ^ 2) y ≤ (fun x => f x + m / 2 * ‖x‖ ^ 2) (a • x + b • y)
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : DecidableEq l<VAR>inst✝ : CommRing R<GOAL>(J l R)ᵀ = -J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : DecidableEq l<VAR>inst✝ : CommRing R<GOAL>fromBlocks 0 1 (-1ᵀ) 0 = fromBlocks (-1 • 0) (-1 • -1) (-1 • 1) (-1 • 0)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>x : R<VAR>hx : x ∈ closure s<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<GOAL>C x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>x : R<VAR>hx : x ∈ closure s<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<GOAL>C x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>L : List (List R)<VAR>HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1<VAR>hx : (List.map List.prod L).sum ∈ closure s<GOAL>C (List.map List.prod L).sum
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : List R<VAR>tl : List (List R)<VAR>ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum<VAR>HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ s ∨ y = -1<GOAL>C (List.map List.prod (hd :: tl)).sum
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : List R<VAR>tl : List (List R)<VAR>ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum<VAR>HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1<GOAL>C (List.map List.prod (hd :: tl)).sum
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : List R<VAR>tl : List (List R)<VAR>ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum<VAR>HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1<GOAL>C hd.prod
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : List R<VAR>tl : List (List R)<VAR>ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum<VAR>HL : ∀ y ∈ hd, y ∈ s ∨ y = -1<GOAL>C hd.prod
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : ∀ y ∈ hd :: tl, y ∈ s ∨ y = -1<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1<VAR>L : List R<VAR>HL' : ∀ x ∈ L, x ∈ s<VAR>HP : tl.prod = L.prod<VAR>hhd : hd ∈ s<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1<VAR>L : List R<VAR>HL' : ∀ x ∈ L, x ∈ s<VAR>HP : tl.prod = L.prod<VAR>hhd : hd = -1<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)