ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<VAR>δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖<VAR>w : ℕ → ↑K<VAR>hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)<VAR>norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)<VAR>seq_is_cauchy : CauchySeq fun n => ↑(w n)<VAR>v : F<VAR>hv : v ∈ K<VAR>w_tendsto : Tendsto (fun n => ↑(w n)) atTop (𝓝 v)<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<VAR>δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖<VAR>w : ℕ → ↑K<VAR>hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)<VAR>norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)<VAR>seq_is_cauchy : CauchySeq fun n => ↑(w n)<VAR>v : F<VAR>hv : v ∈ K<VAR>w_tendsto : Tendsto (fun n => ↑(w n)) atTop (𝓝 v)<GOAL>v ∈ K ∧ ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<VAR>δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖<VAR>w : ℕ → ↑K<VAR>hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)<VAR>norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)<VAR>seq_is_cauchy : CauchySeq fun n => ↑(w n)<VAR>v : F<VAR>hv : v ∈ K<VAR>w_tendsto : Tendsto (fun n => ↑(w n)) atTop (𝓝 v)<GOAL>‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<VAR>δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖<VAR>w : ℕ → ↑K<VAR>hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)<VAR>norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)<VAR>seq_is_cauchy : CauchySeq fun n => ↑(w n)<VAR>v : F<VAR>hv : v ∈ K<VAR>w_tendsto : Tendsto (fun n => ↑(w n)) atTop (𝓝 v)<VAR>h_cont : Continuous fun v => ‖u - v‖<GOAL>‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this✝ : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<VAR>δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖<VAR>w : ℕ → ↑K<VAR>hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)<VAR>norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)<VAR>seq_is_cauchy : CauchySeq fun n => ↑(w n)<VAR>v : F<VAR>hv : v ∈ K<VAR>w_tendsto : Tendsto (fun n => ↑(w n)) atTop (𝓝 v)<VAR>h_cont : Continuous fun v => ‖u - v‖<VAR>this : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 ‖u - v‖)<GOAL>‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>h₂ : a ≤ d<VAR>x : α<GOAL>x ∈ Ioc a b ∪ Ioc c d ↔ x ∈ Ioc (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>h₂ : a ≤ d<VAR>x : α<GOAL>a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ inst✝ : IsLocalization M S<VAR>J : Ideal S<VAR>x : S<VAR>hJ : x ∈ J<GOAL>x ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ inst✝ : IsLocalization M S<VAR>J : Ideal S<VAR>x : S<VAR>hJ : x ∈ J<VAR>r : R<VAR>s : ↥M<VAR>hx : mk' S r s = x<GOAL>x ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ inst✝ : IsLocalization M S<VAR>J : Ideal S<VAR>x : S<VAR>r : R<VAR>s : ↥M<VAR>hJ : mk' S r s ∈ J<VAR>hx : mk' S r s = x<GOAL>mk' S r s ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝¹⁰ : CommRing 𝕜<VAR>inst✝⁹ : NoZeroDivisors 𝕜<VAR>inst✝⁸ : TopologicalSpace 𝕜<VAR>inst✝⁷ : ContinuousAdd 𝕜<VAR>inst✝⁶ : ContinuousConstSMul 𝕜 𝕜<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra 𝕜 A<VAR>inst✝² : Nontrivial 𝕜<VAR>inst✝¹ : T2Space 𝕜<VAR>inst✝ : ContinuousMul 𝕜<GOAL>IsClosed (characterSpace 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝¹⁰ : CommRing 𝕜<VAR>inst✝⁹ : NoZeroDivisors 𝕜<VAR>inst✝⁸ : TopologicalSpace 𝕜<VAR>inst✝⁷ : ContinuousAdd 𝕜<VAR>inst✝⁶ : ContinuousConstSMul 𝕜 𝕜<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra 𝕜 A<VAR>inst✝² : Nontrivial 𝕜<VAR>inst✝¹ : T2Space 𝕜<VAR>inst✝ : ContinuousMul 𝕜<GOAL>IsClosed ({a | a 1 = 1} ∩ {a | ∀ (x y : A), a (x * y) = a x * a y})
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝¹⁰ : CommRing 𝕜<VAR>inst✝⁹ : NoZeroDivisors 𝕜<VAR>inst✝⁸ : TopologicalSpace 𝕜<VAR>inst✝⁷ : ContinuousAdd 𝕜<VAR>inst✝⁶ : ContinuousConstSMul 𝕜 𝕜<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra 𝕜 A<VAR>inst✝² : Nontrivial 𝕜<VAR>inst✝¹ : T2Space 𝕜<VAR>inst✝ : ContinuousMul 𝕜<GOAL>IsClosed {a | ∀ (x y : A), a (x * y) = a x * a y}
<VAR>S : Set ℍ<GOAL>S ∈ atImInfty ↔ ∃ A, ∀ (z : ℍ), A ≤ z.im → z ∈ S
<VAR>S : Set ℍ<GOAL>(∃ i, im ⁻¹' Set.Ici i ⊆ S) ↔ ∃ A, ∀ (z : ℍ), A ≤ z.im → z ∈ S
<VAR>Δ' Δ : SimplexCategory<VAR>i : Δ' ⟶ Δ<VAR>hi : Mono i<VAR>hi' : Δ ≠ Δ'<GOAL>Δ'.len < Δ.len
<VAR>Δ' Δ : SimplexCategory<VAR>i : Δ' ⟶ Δ<VAR>hi : Mono i<VAR>hi' : Δ ≠ Δ'<VAR>h : Δ'.len < Δ.len<GOAL>Δ'.len < Δ.len
<VAR>Δ' Δ : SimplexCategory<VAR>i : Δ' ⟶ Δ<VAR>hi : Mono i<VAR>hi' : Δ ≠ Δ'<VAR>h : Δ'.len = Δ.len<GOAL>Δ'.len < Δ.len
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝³ : CommRing T<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<VAR>p : T[X]<VAR>a : S<GOAL>a ∈ p.aroots S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeAbelianGroup α<GOAL>(map (g ∘ f)) x = (map g) ((map f) x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeAbelianGroup α<GOAL>((map g).comp (map f)) x = (map g) ((map f) x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<GOAL>⨆ i ∈ s, basicOpen i = ⊤ ↔ Ideal.span s = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<GOAL>⨆ i ∈ s, basicOpen i = ⊤ ↔ ⨆ i, basicOpen ↑i = ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>(ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal}) ^ (1 / p.toReal) ≤ eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>(ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal}) ^ (1 / p.toReal) ≤ (∫⁻ (x : α), ↑‖f x‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal} ≤ ∫⁻ (x : α), ↑‖f x‖₊ ^ p.toReal ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f✝ : α → β<VAR>f : β → ↑(Iio a)<GOAL>Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l (𝓝[<] a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f✝ : α → β<VAR>f : β → ↑(Iio a)<GOAL>Tendsto (Subtype.val ∘ f) l (𝓝[<] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[<] a)
<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>m : MeasurableSpace α<VAR>T : Set α → F →L[ℝ] F'<VAR>c : ℝ<VAR>f : α →ₛ F<GOAL>setToSimpleFunc (fun s => c • T s) f = c • setToSimpleFunc T f
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>HasDerivAt (circleMap c R) (circleMap 0 R θ * I) θ
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<VAR>s : Finset F<VAR>hs : LinearIndependent ↥(subfield G F) fun i => ↑i<GOAL>s.card ≤ Fintype.card G
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>inst✝¹ : IsAntisymm α r<VAR>inst✝ : IsTrans α r<VAR>hts : t ⊆ s<VAR>h : ∀ x ∈ s, ∃ y ∈ t, r y x<GOAL>minimals r s = minimals r t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b x : α<VAR>inst✝¹ : IsAntisymm α r<VAR>inst✝ : IsTrans α r<VAR>hts : t ⊆ s<VAR>h : ∀ x ∈ s, ∃ y ∈ t, r y x<VAR>a : α<VAR>x✝ : a ∈ minimals r s<VAR>has : a ∈ s<VAR>hmin : ∀ ⦃b : α⦄, b ∈ s → r b a → r a b<GOAL>a ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝¹ : IsAntisymm α r<VAR>inst✝ : IsTrans α r<VAR>hts : t ⊆ s<VAR>h : ∀ x ∈ s, ∃ y ∈ t, r y x<VAR>a : α<VAR>x✝ : a ∈ minimals r t<VAR>hat : a ∈ t<VAR>hmin : ∀ ⦃b : α⦄, b ∈ t → r b a → r a b<VAR>b : α<VAR>hbs : b ∈ s<VAR>hba : r b a<GOAL>r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝¹ : IsAntisymm α r<VAR>inst✝ : IsTrans α r<VAR>hts : t ⊆ s<VAR>h : ∀ x ∈ s, ∃ y ∈ t, r y x<VAR>a : α<VAR>x✝ : a ∈ minimals r t<VAR>hat : a ∈ t<VAR>hmin : ∀ ⦃b : α⦄, b ∈ t → r b a → r a b<VAR>b : α<VAR>hbs : b ∈ s<VAR>hba : r b a<VAR>b' : α<VAR>hb't : b' ∈ t<VAR>hb'b : r b' b<GOAL>r a b
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>image2 f s (t ∩ t') ∪ image2 f s' (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hq0_lt : 0 < q<VAR>hf_zero : f =ᶠ[ae μ] 0<GOAL>eLpNorm' f q μ = 0
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x✝ : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b : B<VAR>y : E b<VAR>B' : Type u_6<VAR>inst✝ : TopologicalSpace B'<VAR>e : Trivialization F proj<VAR>s : Set B<VAR>x : Z<VAR>hx : x ∈ e.source<GOAL>↑e.toPartialHomeomorph x ∈ s ×ˢ univ ↔ x ∈ proj ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<VAR>n : ℕ<GOAL>nth p n = ↑((Subtype.orderIsoOfNat (setOf p)) n)
<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 L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hg : HasDerivAtFilter g₁ g₁' (h x) L'<VAR>hh : HasDerivAtFilter h h' x L<VAR>hL : Tendsto h L L'<GOAL>HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L
<VAR>b x : Bool<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)<GOAL>count (!b) (x :: l) ≤ count b (x :: l) + 1
<VAR>b : Bool<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) (b :: l)<GOAL>count (!b) (b :: l) ≤ count b (b :: l) + 1
<VAR>x : Bool<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)<GOAL>count (!!x) (x :: l) ≤ count (!x) (x :: l) + 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<GOAL>(ρ_ ((free R).obj X)).hom = (𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).obj (ρ_ X).hom
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<GOAL>(TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ (ρ_ ((free R).obj X)).hom = (TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).obj (ρ_ X).hom)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<GOAL>∀ (a : X), (TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ (ρ_ ((free R).obj X)).hom ∘ₗ Finsupp.lsingle a = (TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).obj (ρ_ X).hom) ∘ₗ Finsupp.lsingle a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<VAR>x : X<GOAL>(TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ (ρ_ ((free R).obj X)).hom ∘ₗ Finsupp.lsingle x = (TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).obj (ρ_ X).hom) ∘ₗ Finsupp.lsingle x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<VAR>x : X<GOAL>((TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ (ρ_ ((free R).obj X)).hom ∘ₗ Finsupp.lsingle x) 1 = ((TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).obj (ρ_ X).hom) ∘ₗ Finsupp.lsingle x) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<VAR>x : X<GOAL>(((TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ (ρ_ ((free R).obj X)).hom ∘ₗ Finsupp.lsingle x) 1) 1 = (((TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).obj (ρ_ X).hom) ∘ₗ Finsupp.lsingle x) 1) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<VAR>x : X<GOAL>∀ (a : X), ((((TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ (ρ_ ((free R).obj X)).hom ∘ₗ Finsupp.lsingle x) 1) 1) a = ((((TensorProduct.mk R ↑((free R).obj X) ↑(𝟙_ (ModuleCat R))).compr₂ ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).obj (ρ_ X).hom) ∘ₗ Finsupp.lsingle x) 1) 1) a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<VAR>x x' : X<VAR>q : X →₀ R := (ρ_ (of R (X →₀ R))).hom (Finsupp.single x 1 ⊗ₜ[R] 1)<GOAL>q x' = (Finsupp.mapDomain (ρ_ X).hom ((finsuppTensorFinsupp' R X (𝟙_ (Type u))) (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single PUnit.unit 1))) x'
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>f : R →+* S<GOAL>((MvPolynomial.map f) φ).IsHomogeneous n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m' : MeasurableSpace β<VAR>inst✝ : BooleanAlgebra β<VAR>h : Measurable compl<VAR>f : α → β<GOAL>MeasurableSpace.comap (fun a => (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m' : MeasurableSpace β<VAR>inst✝ : BooleanAlgebra β<VAR>h : Measurable compl<VAR>f : α → β<GOAL>MeasurableSpace.comap f (MeasurableSpace.comap compl inferInstance) = MeasurableSpace.comap f inferInstance
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m' : MeasurableSpace β<VAR>inst✝ : BooleanAlgebra β<VAR>h : Measurable compl<VAR>f : α → β<GOAL>MeasurableSpace.comap compl inferInstance = inferInstance
<VAR>α β : Type u<VAR>s : Set α<GOAL>#↑(ULift.down ⁻¹' s) = lift.{v, u} #↑s
<VAR>α β : Type u<VAR>s : Set α<GOAL>Nonempty (↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s)
<VAR>α β : Type u<VAR>s : Set α<VAR>f : ↑(ULift.down ⁻¹' s) → ULift.{?u.6919, u} ↑s := fun x => { down := s.restrictPreimage ULift.down x }<GOAL>↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s
<VAR>α β : Type u<VAR>s : Set α<VAR>f : ↑(ULift.down ⁻¹' s) → ULift.{?u.6966, u} ↑s := fun x => { down := s.restrictPreimage ULift.down x }<VAR>this : Bijective f<GOAL>↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>t : Finset β<VAR>a a' : α<VAR>b b' : β<VAR>inst✝¹ : DecidablePred (r a)<VAR>inst✝ : (a : α) → Decidable (r a b)<VAR>m n : ℕ<VAR>hs : ∀ a ∈ s, ∃ b ∈ t, r a b<VAR>ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton<GOAL>s.card ≤ t.card
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ memPartition f n<GOAL>memPartitionSet f n a = s ↔ a ∈ s
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ memPartition f n<VAR>h : a ∈ s<GOAL>memPartitionSet f n a = s
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ memPartition f n<VAR>h : a ∈ s<VAR>h_ne : ¬memPartitionSet f n a = s<GOAL>False
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ memPartition f n<VAR>h : a ∈ s<VAR>h_ne : ¬memPartitionSet f n a = s<VAR>h_disj : Disjoint s (memPartitionSet f n a)<GOAL>False
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ memPartition f n<VAR>h : a ∈ s<VAR>h_ne : ¬memPartitionSet f n a = s<VAR>h_disj : Disjoint s (memPartitionSet f n a)<GOAL>¬Disjoint s (memPartitionSet f n a)
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ memPartition f n<VAR>h : a ∈ s<VAR>h_ne : ¬memPartitionSet f n a = s<VAR>h_disj : Disjoint s (memPartitionSet f n a)<GOAL>(s ∩ memPartitionSet f n a).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : _root_.Embedding f<VAR>hg : _root_.Embedding g<VAR>x✝¹ x✝ : X × Z<VAR>x₁ : X<VAR>z₁ : Z<VAR>x₂ : X<VAR>z₂ : Z<GOAL>Prod.map f g (x₁, z₁) = Prod.map f g (x₂, z₂) → (x₁, z₁) = (x₂, z₂)
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>α : Type u_4<VAR>β : Type u_5<GOAL>IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β
<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>r : α → α → Prop<VAR>a b c d : α<GOAL>ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b
<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>r : α → α → Prop<VAR>a b c d : α<GOAL>(a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) → ReflTransGen r a b
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b : WithTop α<VAR>hb : b ≠ 0<GOAL>⊤ * b = ⊤
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hw : w i ≠ 0<GOAL>{i}.centerMass w z = z i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n✝ : ℕ<VAR>x y : List α<VAR>h : x <+: y<VAR>n : ℕ<VAR>hn : n < x.length<GOAL>x.get ⟨n, hn⟩ = y.get ⟨n, ⋯⟩
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>inst✝ : NeZero n<VAR>a : Fin (n + 1)<VAR>b : Fin n<VAR>ha : a ≠ 0<GOAL>a.succAbove b = 0 ↔ b = 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a x y x' y' : G₀<VAR>h : SemiconjBy a x y<VAR>h' : SemiconjBy a x' y'<GOAL>SemiconjBy a (x / x') (y / y')
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a x y x' y' : G₀<VAR>h : SemiconjBy a x y<VAR>h' : SemiconjBy a x' y'<GOAL>SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A✝ : Rep k G✝<VAR>G : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : MulAction G A<VAR>f : G → A<VAR>hf : IsOneCocycle f<VAR>g : G<GOAL>g • f g⁻¹ = -f g