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>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>a✝¹ : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>((κ a✝¹).withDensity (0 a✝¹)) s✝ = (0 a✝¹) s✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>f : (i : ℕ) → i < n → α<VAR>hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a<VAR>hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s<VAR>f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j<GOAL>s.ncard = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>f : (i : ℕ) → i < n → α<VAR>hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a<VAR>hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s<VAR>f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j<VAR>f' : Fin n → α := fun i => f ↑i ⋯<GOAL>s.ncard = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>f : (i : ℕ) → i < n → α<VAR>hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a<VAR>hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s<VAR>f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j<VAR>f' : Fin n → α := fun i => f ↑i ⋯<GOAL>s = f' '' univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>f : (i : ℕ) → i < n → α<VAR>hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a<VAR>hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s<VAR>f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j<VAR>f' : Fin n → α := fun i => f ↑i ⋯<VAR>x : α<GOAL>x ∈ s ↔ x ∈ f' '' univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>f : (i : ℕ) → i < n → α<VAR>hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a<VAR>hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s<VAR>f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j<VAR>f' : Fin n → α := fun i => f ↑i ⋯<VAR>x : α<GOAL>x ∈ s ↔ ∃ y, f' y = x
<VAR>R : Type u<VAR>a b : R<VAR>m✝ n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>k l m n : ℕ<VAR>u v : R<VAR>hu : u ≠ 0<VAR>hv : v ≠ 0<GOAL>C u * X ^ k + C v * X ^ l = C u * X ^ m + C v * X ^ n ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
<VAR>R : Type u<VAR>a b : R<VAR>m✝ n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>k l m n : ℕ<VAR>u v : R<VAR>hu : u ≠ 0<VAR>hv : v ≠ 0<GOAL>Finsupp.single k u + Finsupp.single l v = Finsupp.single m u + Finsupp.single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
<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>c : E<VAR>f✝ : α → E<VAR>hf✝ : AEStronglyMeasurable f✝ μ<VAR>s✝ : Set α<VAR>p q : ℝ≥0∞<VAR>f : α → E<VAR>hfq : Memℒp f q μ<VAR>s : Set α<VAR>hf : ∀ x ∉ s, f x = 0<VAR>hs : μ s ≠ ⊤<VAR>hpq : p ≤ q<GOAL>Memℒp f p μ
<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>c : E<VAR>f✝ : α → E<VAR>hf✝ : AEStronglyMeasurable f✝ μ<VAR>s✝ : Set α<VAR>p q : ℝ≥0∞<VAR>f : α → E<VAR>hfq : Memℒp f q μ<VAR>s : Set α<VAR>hf : ∀ x ∉ s, f x = 0<VAR>hs : μ s ≠ ⊤<VAR>hpq : p ≤ q<VAR>this : (toMeasurable μ s).indicator f = f<GOAL>Memℒp f p μ
<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>c : E<VAR>f✝ : α → E<VAR>hf✝ : AEStronglyMeasurable f✝ μ<VAR>s✝ : Set α<VAR>p q : ℝ≥0∞<VAR>f : α → E<VAR>s : Set α<VAR>hfq : Memℒp f q (μ.restrict (toMeasurable μ s))<VAR>hf : ∀ x ∉ s, f x = 0<VAR>hs : μ s ≠ ⊤<VAR>hpq : p ≤ q<VAR>this : (toMeasurable μ s).indicator f = f<GOAL>Memℒp f p (μ.restrict (toMeasurable μ s))
<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>c : E<VAR>f✝ : α → E<VAR>hf✝ : AEStronglyMeasurable f✝ μ<VAR>s✝ : Set α<VAR>p q : ℝ≥0∞<VAR>f : α → E<VAR>s : Set α<VAR>hfq : Memℒp f q (μ.restrict (toMeasurable μ s))<VAR>hf : ∀ x ∉ s, f x = 0<VAR>hs : μ s ≠ ⊤<VAR>hpq : p ≤ q<VAR>this✝ : (toMeasurable μ s).indicator f = f<VAR>this : Fact (μ (toMeasurable μ s) < ⊤)<GOAL>Memℒp f p (μ.restrict (toMeasurable μ s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>h : OpenEmbedding f<VAR>s : Set α<GOAL>IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>h : OpenEmbedding f<VAR>s : Set α<GOAL>IsQuasiSeparated (f '' s) → IsQuasiSeparated s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>h : OpenEmbedding f<VAR>s : Set α<VAR>H : IsQuasiSeparated (f '' s)<VAR>U V : Set α<VAR>hU : U ⊆ s<VAR>hU' : IsOpen U<VAR>hU'' : IsCompact U<VAR>hV : V ⊆ s<VAR>hV' : IsOpen V<VAR>hV'' : IsCompact V<GOAL>IsCompact (U ∩ V)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>h : OpenEmbedding f<VAR>s : Set α<VAR>H : IsQuasiSeparated (f '' s)<VAR>U V : Set α<VAR>hU : U ⊆ s<VAR>hU' : IsOpen U<VAR>hU'' : IsCompact U<VAR>hV : V ⊆ s<VAR>hV' : IsOpen V<VAR>hV'' : IsCompact V<GOAL>IsCompact (f '' U ∩ f '' V)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Countable ι'<VAR>s : ι' → Set X<VAR>T : ι' → Set (Set X)<VAR>hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen t<VAR>hTc : ∀ (i : ι'), (T i).Countable<VAR>hTs : ∀ (i : ι'), s i = ⋂₀ T i<GOAL>IsGδ (⋂ i, s i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Countable ι'<VAR>T : ι' → Set (Set X)<VAR>hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen t<VAR>hTc : ∀ (i : ι'), (T i).Countable<VAR>hTs : ∀ (i : ι'), (fun i => ⋂₀ T i) i = ⋂₀ T i<GOAL>IsGδ (⋂ i, (fun i => ⋂₀ T i) i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Countable ι'<VAR>T : ι' → Set (Set X)<VAR>hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen t<VAR>hTc : ∀ (i : ι'), (T i).Countable<VAR>hTs : ∀ (i : ι'), (fun i => ⋂₀ T i) i = ⋂₀ T i<GOAL>∀ t ∈ ⋃ i, T i, IsOpen t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hf_tendsto : Tendsto (fun n => eLpNorm (f n) p μ) atTop (𝓝 0)<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hN : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ENNReal.ofReal ε<VAR>F : Fin N → α → β := fun n => f ↑n<VAR>hF : ∀ (n : Fin N), Memℒp (F n) p μ<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hN : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ENNReal.ofReal ε<VAR>F : Fin N → α → β := fun n => f ↑n<VAR>hF : ∀ (n : Fin N), Memℒp (F n) p μ<VAR>δ₁ : ℝ<VAR>hδpos₁ : 0 < δ₁<VAR>hδ₁ : ∀ (i : Fin N) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (F i)) p μ ≤ ENNReal.ofReal ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Nonempty X<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : MeasurableSpace.CountablySeparated X<VAR>f : α → α<VAR>g : α → X<VAR>h : PreErgodic f μ<VAR>hgm : Measurable g<VAR>hg_eq : g ∘ f = g<VAR>U : Set X<VAR>hU : MeasurableSet U<GOAL>f ⁻¹' (g ⁻¹' U) = g ⁻¹' U
<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>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>n : ℕ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>mα.prod (↑(countableFiltration γ) n) ≤ Prod.instMeasurableSpace
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>h : angle x y = π<GOAL>‖x - y‖ = ‖x‖ + ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>h : angle x y = π<GOAL>‖x‖ ^ 2 - 2 * -(‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle x (r • x - y)).sign = -(o.oangle x y).sign
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : AddCommMonoid R<VAR>s : Multiset (Tropical R)<GOAL>∀ (a : List (Tropical R)), untrop (prod ⟦a⟧) = (map untrop ⟦a⟧).sum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<GOAL>(fun x => (u x)⁻¹) ~[l] fun x => (v x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>huv : ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v<GOAL>∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>φ : α → β<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>h : u =ᶠ[l] φ * v<GOAL>∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>φ : α → β<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>h : u =ᶠ[l] φ * v<GOAL>∃ φ, ∃ (_ : Tendsto φ l (𝓝 1⁻¹)), (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>φ : α → β<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>h : u =ᶠ[l] φ * v<GOAL>(fun x => (u x)⁻¹) =ᶠ[l] (fun x => (φ x)⁻¹) * fun x => (v x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>φ : α → β<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>h : u =ᶠ[l] φ * v<VAR>x✝ : α<GOAL>((fun x => (φ x)⁻¹) * fun x => (v x)⁻¹) x✝ = ((φ * v) x✝)⁻¹
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>f : F[X]<VAR>h : Irreducible f<VAR>H : f.natDegree = 0<GOAL>False
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>f : F[X]<VAR>h : Irreducible f<VAR>H : f.natDegree = 0<VAR>x : F<VAR>hf : C x = f<GOAL>False
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>f : F[X]<VAR>h : Irreducible f<VAR>H : f.natDegree = 0<VAR>x : F<VAR>hf : C x = f<VAR>hx : ¬x = 0<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>h : a ≠ b<VAR>l : List α<GOAL>count a (b :: l) = count a l
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : ContinuousAdd M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : Nontrivial M<VAR>inst✝¹ : (𝓝[≠] 0).NeBot<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<GOAL>(𝓝[≠] x).NeBot
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : ContinuousAdd M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : Nontrivial M<VAR>inst✝¹ : (𝓝[≠] 0).NeBot<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>(𝓝[≠] x).NeBot
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : ContinuousAdd M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : Nontrivial M<VAR>inst✝¹ : (𝓝[≠] 0).NeBot<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>Tendsto (fun c => x + c • y) (𝓝[≠] 0) (𝓝[≠] x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : ContinuousAdd M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : Nontrivial M<VAR>inst✝¹ : (𝓝[≠] 0).NeBot<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>Tendsto (fun c => x + c • y) (𝓝 0) (𝓝 x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : ContinuousAdd M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : Nontrivial M<VAR>inst✝¹ : (𝓝[≠] 0).NeBot<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>∀ a ∈ {0}ᶜ, x + a • y ∈ {x}ᶜ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite ι'<VAR>h : (i : ι) → MeasurableSpace (α i)<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), generateFrom (C i) = h i<VAR>h2C : ∀ (i : ι), IsCountablySpanning (C i)<GOAL>generateFrom (univ.pi '' univ.pi C) = MeasurableSpace.pi
<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DivisionRing α<VAR>a : ↥(closure s)<VAR>x✝ : a ∈ ⊤<GOAL>a ∈ Subfield.rangeOfWType s
<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DivisionRing α<VAR>a : ↥(closure s)<VAR>x✝ : a ∈ ⊤<GOAL>↑a ∈ Subtype.val '' ↑(Subfield.rangeOfWType s)
<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DivisionRing α<VAR>a : ↥(closure s)<VAR>x✝ : a ∈ ⊤<GOAL>↑a ∈ map (closure s).subtype (Subfield.rangeOfWType s)
<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DivisionRing α<VAR>a✝ : ↥(closure s)<VAR>x✝ : a✝ ∈ ⊤<VAR>a : α<VAR>ha : a ∈ s<GOAL>a ∈ ↑(map (closure s).subtype (Subfield.rangeOfWType s))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<GOAL>truncateFun n (x * y) = truncateFun n x * truncateFun n y
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>χ : LieCharacter R L<VAR>x : L<VAR>h : x ∈ derivedSeries R L 1<GOAL>χ x = 0
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>χ : LieCharacter R L<VAR>x : L<VAR>h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}<GOAL>χ x = 0
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>χ : LieCharacter R L<VAR>x : L<VAR>h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}<GOAL>∀ x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}, χ x = 0
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>χ : LieCharacter R L<VAR>x : L<VAR>h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}<GOAL>χ 0 = 0
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>χ : LieCharacter R L<VAR>x : L<VAR>h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}<GOAL>∀ (x y : L), χ x = 0 → χ y = 0 → χ (x + y) = 0
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>χ : LieCharacter R L<VAR>x : L<VAR>h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}<GOAL>∀ (a : R) (x : L), χ x = 0 → χ (a • x) = 0
<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>s : Set E<VAR>x : E<VAR>inst✝ : Fintype ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hw₀ : ∀ (i : ι), 0 ≤ w i<VAR>hw₁ : ∑ i : ι, w i = 1<VAR>hz : ∀ (i : ι), z i ∈ s<VAR>hx : ∑ i : ι, w i • z i = x<GOAL>x ∈ (convexHull R) s
<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>s : Set E<VAR>x : E<VAR>inst✝ : Fintype ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hw₀ : ∀ (i : ι), 0 ≤ w i<VAR>hw₁ : ∑ i : ι, w i = 1<VAR>hz : ∀ (i : ι), z i ∈ s<VAR>hx : ∑ i : ι, w i • z i = x<GOAL>Finset.univ.centerMass w z ∈ (convexHull R) s
<VAR>R : Type u_1<VAR>inst✝ : CommGroupWithZero R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>(f.pdiv g) (m * n) = (f.pdiv g) m * (f.pdiv g) n
<VAR>R : Type u_1<VAR>inst✝ : CommGroupWithZero R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>f m * f n * ((g m)⁻¹ * (g n)⁻¹) = f m * (g m)⁻¹ * (f n * (g n)⁻¹)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.edges = p.edges.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionSemiring α<VAR>q : ℚ≥0<GOAL>q • 1 = ↑q
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hf₀ : 0 ≤ᶠ[ae μ] f<GOAL>ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ univ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>ν : Measure α<VAR>s t : Set α<VAR>f : α → ℝ<VAR>hf : Integrable f 0<VAR>hf₀ : 0 ≤ᶠ[ae 0] f<GOAL>ENNReal.ofReal (⨍ (x : α), f x ∂0) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂0) / 0 univ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hf₀ : 0 ≤ᶠ[ae μ] f<VAR>hμ : μ ≠ 0<GOAL>ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ univ
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>L : IntermediateField F E<GOAL>L ≤ perfectClosure F E ↔ IsPurelyInseparable F ↥L
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>L : IntermediateField F E<VAR>h : L ≤ perfectClosure F E<VAR>x : ↥L<GOAL>∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>L : IntermediateField F E<VAR>h : L ≤ perfectClosure F E<VAR>x : ↥L<VAR>n : ℕ<VAR>y : F<VAR>hy : (algebraMap F E) y = ↑x ^ ringExpChar F ^ n<GOAL>∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : Measure.map X ℙ = gaussianReal μ v<VAR>c : ℝ<VAR>hXm : AEMeasurable X ℙ<GOAL>Measure.map (fun ω => c * X ω) ℙ = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : Measure.map X ℙ = gaussianReal μ v<VAR>c : ℝ<VAR>hXm : AEMeasurable X ℙ<GOAL>Measure.map ((fun ω => c * ω) ∘ X) ℙ = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : Measure.map X ℙ = gaussianReal μ v<VAR>c : ℝ<VAR>hXm : AEMeasurable X ℙ<GOAL>Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>x : R<VAR>hx : x ∈ I.jacobson<VAR>y : R<VAR>hxy : I ⊔ span {y * x + 1} = ⊤<VAR>p : R<VAR>hpi : p ∈ I<VAR>q : R<VAR>hq : q ∈ span {y * x + 1}<VAR>hpq : p + q = 1<VAR>r : R<VAR>hr : r * (y * x + 1) = q<GOAL>r * y * x + r - 1 ∈ I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>x : R<VAR>hx : x ∈ I.jacobson<VAR>y : R<VAR>hxy : I ⊔ span {y * x + 1} = ⊤<VAR>p : R<VAR>hpi : p ∈ I<VAR>q : R<VAR>hq : q ∈ span {y * x + 1}<VAR>hpq : p + q = 1<VAR>r : R<VAR>hr : r * (y * x + 1) = q<GOAL>-p ∈ I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>x : R<VAR>hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I<VAR>M : Ideal R<VAR>x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}<VAR>him : I ≤ M<VAR>hm : M.IsMaximal<VAR>hxm : x ∉ M<VAR>y i : R<VAR>hi : i ∈ M<VAR>df : y * x + i = 1<VAR>z : R<VAR>hz : z * -y * x + z - 1 ∈ I<GOAL>z * -y * x + z ∈ M
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>x : R<VAR>hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I<VAR>M : Ideal R<VAR>x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}<VAR>him : I ≤ M<VAR>hm : M.IsMaximal<VAR>hxm : x ∉ M<VAR>y i : R<VAR>hi : i ∈ M<VAR>df : y * x + i = 1<VAR>z : R<VAR>hz : z * -y * x + z - 1 ∈ I<GOAL>z * i ∈ M
<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>p : ℝ≥0∞<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
<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>p : ℝ≥0∞<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>eLpNorm' f p.toReal (c • μ) = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ