ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u<VAR>R✝ : Type v<VAR>inst✝² : CommSemiring R✝<VAR>p✝ m : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : R →+* S<VAR>n : σ →₀ ℕ<VAR>x✝ : n ∈ p.support<GOAL>Finsupp.mapRange ⇑f ⋯ ((monomial n) (coeff n p)) = (map f) ((monomial n) (coeff n p))
<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<GOAL>(o.oangle (x + y) y).sign = (o.oangle x y).sign
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Infinite k<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module k E<VAR>s : Finset (Subspace k E)<VAR>hcovers : ⋃ p ∈ s, ↑p = Set.univ<GOAL>∃ p ∈ s, p = ⊤
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Infinite k<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module k E<VAR>s : Finset (Subspace k E)<VAR>hcovers : ∀ p ∈ s, p ≠ ⊤<GOAL>⋃ p ∈ s, ↑p ≠ Set.univ
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ = 0
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂<GOAL>c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂
<VAR>x y : ℂ<GOAL>cexp (x + y) = cexp x * cexp y
<VAR>x y : ℂ<VAR>hj : ∀ (j : ℕ), ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial = ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)<GOAL>cexp (x + y) = cexp x * cexp y
<VAR>x y : ℂ<VAR>hj : ∀ (j : ℕ), ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial = ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)<GOAL>CauSeq.lim ⟨fun n => ∑ m ∈ range n, (x + y) ^ m / ↑m.factorial, ⋯⟩ = (⟨fun n => ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n => ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩).lim
<VAR>x y : ℂ<VAR>hj : ∀ (j : ℕ), ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial = ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)<GOAL>⟨fun n => ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n => ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩ ≈ ⟨fun n => ∑ m ∈ range n, (x + y) ^ m / ↑m.factorial, ⋯⟩
<VAR>x y : ℂ<VAR>hj : ∀ (j : ℕ), ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial = ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)<GOAL>⟨fun n => ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n => ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩ ≈ ⟨fun n => ∑ i ∈ range n, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial), ⋯⟩
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<GOAL>(𝓝 1).HasBasis (fun V => V ∈ B) id
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<GOAL>toFilterBasis.filter.HasBasis (fun V => V ∈ B) id
<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>x✝ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : Countable δ<VAR>l : Filter δ<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>l' : Filter γ<VAR>inst✝ : l'.IsCountablyGenerated<VAR>hl' : l'.IsMeasurablyGenerated<VAR>f : δ → β → γ<VAR>hf : ∀ (i : δ), Measurable (f i)<GOAL>MeasurableSet {x | Tendsto (fun n => f n x) l l'}
<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>x✝ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : Countable δ<VAR>l : Filter δ<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>l' : Filter γ<VAR>inst✝ : l'.IsCountablyGenerated<VAR>hl' : l'.IsMeasurablyGenerated<VAR>f : δ → β → γ<VAR>hf : ∀ (i : δ), Measurable (f i)<VAR>u : ℕ → Set δ<VAR>hu : l.HasAntitoneBasis u<GOAL>MeasurableSet {x | Tendsto (fun n => f n x) l l'}
<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>x✝ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : Countable δ<VAR>l : Filter δ<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>l' : Filter γ<VAR>inst✝ : l'.IsCountablyGenerated<VAR>hl' : l'.IsMeasurablyGenerated<VAR>f : δ → β → γ<VAR>hf : ∀ (i : δ), Measurable (f i)<VAR>u : ℕ → Set δ<VAR>hu : l.HasAntitoneBasis u<VAR>v : ℕ → Set γ<VAR>v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)<VAR>hv : l'.HasAntitoneBasis fun i => id (v i)<GOAL>MeasurableSet {x | Tendsto (fun n => f n x) l l'}
<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>x✝ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : Countable δ<VAR>l : Filter δ<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>l' : Filter γ<VAR>inst✝ : l'.IsCountablyGenerated<VAR>hl' : l'.IsMeasurablyGenerated<VAR>f : δ → β → γ<VAR>hf : ∀ (i : δ), Measurable (f i)<VAR>u : ℕ → Set δ<VAR>hu : l.HasAntitoneBasis u<VAR>v : ℕ → Set γ<VAR>v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)<VAR>hv : l'.HasAntitoneBasis fun i => id (v i)<GOAL>MeasurableSet (⋂ i, ⋃ i_1, ⋂ i_2 ∈ u i_1, {x | f i_2 x ∈ id (v i)})
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasImage g<VAR>inst✝ : HasImage (f ≫ g)<GOAL>lift (MonoFactorisation.mk (image g) (ι g) (f ≫ factorThruImage g) ⋯) ≫ ι g = ι (f ≫ g)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : Ω[S⁄R]<GOAL>∃ a, (D R S).tensorProductTo a = x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : ↥(ideal R S)<GOAL>∃ a, (D R S).tensorProductTo a = (ideal R S).toCotangent x
<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 x y : α<GOAL>x ⊔ y = ⨆ b, bif b then x else y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>n✝ n : ℕ<VAR>ihn : id^[n] = id<GOAL>id^[n.succ] = id
<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>ι : Type u_9<VAR>a : α<VAR>s : Set ι<VAR>hs : s.Nonempty<GOAL>⨆ i ∈ s, a = a
<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>ι : Type u_9<VAR>a : α<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<GOAL>⨆ i ∈ s, a = a
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>P : Sylow p G<GOAL>P ∈ fixedPoints (↥H) (Sylow p G) ↔ H ≤ (↑P).normalizer
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>P : Sylow p G<GOAL>P ∈ fixedPoints (↥H) (Sylow p G) ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>l : Filter X<GOAL>Tendsto pure l (𝓝 l)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>l : Filter X<GOAL>∀ s ∈ l, ∀ᶠ (a : X) in l, s ∈ pure a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>s : Submonoid M<VAR>t : Submonoid N<GOAL>s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤
<VAR>x : ℝ<VAR>n : ℤ<GOAL>↑(↑n * x) = n • ↑x
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>eraseP p l = erasePTR p l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>eraseP p l = erasePTR.go p l l #[]
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>Xs : ι → Set α<GOAL>M.closure (⋃ i, M.closure (Xs i)) = M.closure (⋃ i, Xs i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>Xs : ι → Set α<GOAL>M.subtypeClosure ⟨⋃ i, ↑(M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩) ∩ M.E, ⋯⟩ = M.subtypeClosure ⟨⋃ i, Xs i ∩ M.E, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<GOAL>insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, eLpNorm (f - ⇑g) p μ ≤ ε ∧ Memℒp (⇑g) p μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∀ (f g : α → E), Continuous f ∧ Memℒp f p μ ∧ IsBounded (range f) → Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g) → Continuous (f + g) ∧ Memℒp (f + g) p μ ∧ IsBounded (range (f + g))
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∀ (f : α → E), Continuous f ∧ Memℒp f p μ ∧ IsBounded (range f) → AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>δ : ℝ≥0∞<VAR>δpos : 0 < δ<VAR>hδ : ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>δ : ℝ≥0∞<VAR>δpos : 0 < δ<VAR>hδ : ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε<VAR>η : ℝ≥0<VAR>ηpos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>δ : ℝ≥0∞<VAR>δpos : 0 < δ<VAR>hδ : ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε<VAR>η : ℝ≥0<VAR>ηpos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ<VAR>hη_pos' : 0 < ↑η<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>δ : ℝ≥0∞<VAR>δpos : 0 < δ<VAR>hδ : ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε<VAR>η : ℝ≥0<VAR>ηpos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ<VAR>hη_pos' : 0 < ↑η<VAR>s : Set α<VAR>st : s ⊆ t<VAR>s_closed : IsClosed s<VAR>μs : μ (t \ s) < ↑η<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>δ : ℝ≥0∞<VAR>δpos : 0 < δ<VAR>hδ : ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε<VAR>η : ℝ≥0<VAR>ηpos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ<VAR>hη_pos' : 0 < ↑η<VAR>s : Set α<VAR>st : s ⊆ t<VAR>s_closed : IsClosed s<VAR>μs : μ (t \ s) < ↑η<VAR>hsμ : μ s < ⊤<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>δ : ℝ≥0∞<VAR>δpos : 0 < δ<VAR>hδ : ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε<VAR>η : ℝ≥0<VAR>ηpos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ<VAR>hη_pos' : 0 < ↑η<VAR>s : Set α<VAR>st : s ⊆ t<VAR>s_closed : IsClosed s<VAR>μs : μ (t \ s) < ↑η<VAR>hsμ : μ s < ⊤<VAR>I1 : eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f✝ : α → E<VAR>hf : Memℒp f✝ p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>δ : ℝ≥0∞<VAR>δpos : 0 < δ<VAR>hδ : ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε<VAR>η : ℝ≥0<VAR>ηpos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ<VAR>hη_pos' : 0 < ↑η<VAR>s : Set α<VAR>st : s ⊆ t<VAR>s_closed : IsClosed s<VAR>μs : μ (t \ s) < ↑η<VAR>hsμ : μ s < ⊤<VAR>I1 : eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ<VAR>f : α → E<VAR>f_cont : Continuous f<VAR>I2 : eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ δ<VAR>f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖<VAR>f_mem : Memℒp f p μ<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f✝ : α → E<VAR>hf : Memℒp f✝ p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>δ : ℝ≥0∞<VAR>δpos : 0 < δ<VAR>hδ : ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε<VAR>η : ℝ≥0<VAR>ηpos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ<VAR>hη_pos' : 0 < ↑η<VAR>s : Set α<VAR>st : s ⊆ t<VAR>s_closed : IsClosed s<VAR>μs : μ (t \ s) < ↑η<VAR>hsμ : μ s < ⊤<VAR>I1 : eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ<VAR>f : α → E<VAR>f_cont : Continuous f<VAR>I2 : eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ δ<VAR>f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖<VAR>f_mem : Memℒp f p μ<VAR>I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ IsBounded (range g)
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f✝ : α → E<VAR>hf : Memℒp f✝ p μ<VAR>ε✝ : ℝ≥0∞<VAR>hε✝ : ε✝ ≠ 0<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>htμ : μ t < ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>δ : ℝ≥0∞<VAR>δpos : 0 < δ<VAR>hδ : ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε<VAR>η : ℝ≥0<VAR>ηpos : 0 < η<VAR>hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ<VAR>hη_pos' : 0 < ↑η<VAR>s : Set α<VAR>st : s ⊆ t<VAR>s_closed : IsClosed s<VAR>μs : μ (t \ s) < ↑η<VAR>hsμ : μ s < ⊤<VAR>I1 : eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ<VAR>f : α → E<VAR>f_cont : Continuous f<VAR>I2 : eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ δ<VAR>f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖<VAR>f_mem : Memℒp f p μ<VAR>I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε<GOAL>IsBounded (range f)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z : ℝ≥0∞<VAR>h1 : y ≠ 0<VAR>h2 : y ≠ ⊤<GOAL>x / y ≤ z ↔ x ≤ z * y
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝¹⁷ : Semiring R₁<VAR>inst✝¹⁶ : Semiring R₂<VAR>inst✝¹⁵ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M₁<VAR>inst✝¹³ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹² : TopologicalSpace M'₁<VAR>inst✝¹¹ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace M₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝⁸ : TopologicalSpace M₃<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁶ : TopologicalSpace M₄<VAR>inst✝⁵ : AddCommMonoid M₄<VAR>inst✝⁴ : Module R₁ M₁<VAR>inst✝³ : Module R₁ M'₁<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>inst✝ : ContinuousAdd M₂<VAR>ι : Type u_9<VAR>t : Finset ι<VAR>f : ι → M₁ →SL[σ₁₂] M₂<VAR>b : M₁<GOAL>(∑ d ∈ t, f d) b = ∑ d ∈ t, (f d) b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≠ ⊤<GOAL>⊤ / a = ⊤
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<GOAL>x.valMinAbs.natAbs ≤ n / 2
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<GOAL>↑x.valMinAbs.natAbs * 2 ≤ ↑n
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<VAR>h : x.valMinAbs = ↑x.valMinAbs.natAbs<GOAL>↑x.valMinAbs.natAbs * 2 ≤ ↑n
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<VAR>h : x.valMinAbs = -↑x.valMinAbs.natAbs<GOAL>↑x.valMinAbs.natAbs * 2 ≤ ↑n
<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>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<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✝² : SeminormedRing R'<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedField 𝕜'<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>l l' : Filter α<VAR>h : f'' =Θ[l] g''<GOAL>Tendsto f'' l (𝓝 0) ↔ Tendsto g'' l (𝓝 0)
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>x : Fin (n + 1)<VAR>y : Fin n<GOAL>x.succAbove y ≠ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionRing K<VAR>a b c d : K<VAR>hbc : Commute b c<VAR>hbd : Commute b d<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<GOAL>a / b - c / d = (a * d - b * c) / (b * d)