ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>hz_re : 0 ≤ z.re<VAR>hz_im : z.im ≤ 0<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ (-z).re<VAR>hz_im : (-z).im ≤ 0<GOAL>‖f (-z)‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : z.re ≤ 0<VAR>hz_im : 0 ≤ z.im<GOAL>‖f (-z)‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : z.re ≤ 0<VAR>hz_im : 0 ≤ z.im<GOAL>‖(f ∘ Neg.neg) z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : z.re ≤ 0<VAR>hz_im : 0 ≤ z.im<VAR>H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)<GOAL>‖(f ∘ Neg.neg) z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : z.re ≤ 0<VAR>hz_im : 0 ≤ z.im<VAR>H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)<GOAL>∃ c < 2, ∃ B, (f ∘ Neg.neg) =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : z.re ≤ 0<VAR>hz_im : 0 ≤ z.im<VAR>H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>‖(f ∘ Neg.neg) ↑x‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : z.re ≤ 0<VAR>hz_im : 0 ≤ z.im<VAR>H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>‖(f ∘ Neg.neg) (↑x * I)‖ ≤ C
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F TotalSpace.proj<VAR>this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this : FiberBundle F E := a.toFiberBundle<GOAL>Continuous TotalSpace.proj
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>w x y✝ z✝ : α<VAR>hwx : w ≠ x<VAR>hyz✝ : y✝ ≠ z✝<VAR>y z : α<VAR>hyz : y ≠ z<VAR>hwz : w ≠ z<GOAL>swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>w x y z : α<VAR>hwx : w ≠ x<VAR>hyz : y ≠ z<VAR>h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z<VAR>hwz : w = z<GOAL>z ≠ y
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>w x y z : α<VAR>hwx : w ≠ x<VAR>hyz : y ≠ z<VAR>h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z<VAR>hwz : w = z<VAR>hwy : w ≠ y<GOAL>swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap y z
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>s : Set Y<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<GOAL>Tendsto (fun a => μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s))) l (𝓝 0)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>s : Set Y<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>this : ν.InnerRegularCompactLTTop<GOAL>Tendsto (fun a => μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s))) l (𝓝 0)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>s : Set Y<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>this : ν.InnerRegularCompactLTTop<GOAL>∀ ε > 0, ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<GOAL>∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<VAR>hνs' : μ (⇑g ⁻¹' s) ≠ ⊤<GOAL>∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<VAR>hνs' : μ (⇑g ⁻¹' s) ≠ ⊤<VAR>K : Set X<VAR>hKg : MapsTo (⇑g) K s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2<GOAL>∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<VAR>hνs' : μ (⇑g ⁻¹' s) ≠ ⊤<VAR>K : Set X<VAR>hKg : MapsTo (⇑g) K s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2<VAR>hKm : MeasurableSet K<GOAL>∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<VAR>hνs' : μ (⇑g ⁻¹' s) ≠ ⊤<VAR>K : Set X<VAR>hKg : MapsTo (⇑g) K s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2<VAR>hKm : MeasurableSet K<VAR>a : α<VAR>hfa : MeasurePreserving (⇑(f a)) μ ν<VAR>ha : MapsTo (⇑(f a)) K s<GOAL>μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<VAR>hνs' : μ (⇑g ⁻¹' s) ≠ ⊤<VAR>K : Set X<VAR>hKg : MapsTo (⇑g) K s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2<VAR>hKm : MeasurableSet K<VAR>a : α<VAR>hfa : MeasurePreserving (⇑(f a)) μ ν<VAR>ha : MapsTo (⇑(f a)) K s<GOAL>μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε / 2 + ε / 2
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<VAR>hνs' : μ (⇑g ⁻¹' s) ≠ ⊤<VAR>K : Set X<VAR>hKg : MapsTo (⇑g) K s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2<VAR>hKm : MeasurableSet K<VAR>a : α<VAR>hfa : MeasurePreserving (⇑(f a)) μ ν<VAR>ha : MapsTo (⇑(f a)) K s<GOAL>μ ((⇑(f a) ⁻¹' s) ∆ K) + μ (K ∆ (⇑g ⁻¹' s)) ≤ ε / 2 + ε / 2
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<VAR>hνs' : μ (⇑g ⁻¹' s) ≠ ⊤<VAR>K : Set X<VAR>hKg : MapsTo (⇑g) K s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2<VAR>hKm : MeasurableSet K<VAR>a : α<VAR>hfa : MeasurePreserving (⇑(f a)) μ ν<VAR>ha : MapsTo (⇑(f a)) K s<GOAL>μ (⇑(f a) ⁻¹' s \ K) + μ (⇑g ⁻¹' s \ K) ≤ ε / 2 + ε / 2
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<VAR>hνs' : μ (⇑g ⁻¹' s) ≠ ⊤<VAR>K : Set X<VAR>hKg : MapsTo (⇑g) K s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2<VAR>hKm : MeasurableSet K<VAR>a : α<VAR>hfa : MeasurePreserving (⇑(f a)) μ ν<VAR>ha : MapsTo (⇑(f a)) K s<GOAL>μ (⇑(f a) ⁻¹' s \ K) ≤ ε / 2
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<VAR>hνs' : μ (⇑g ⁻¹' s) ≠ ⊤<VAR>K : Set X<VAR>hKg : MapsTo (⇑g) K s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2<VAR>hKm : MeasurableSet K<VAR>a : α<VAR>hfa : MeasurePreserving (⇑(f a)) μ ν<VAR>ha : MapsTo (⇑(f a)) K s<VAR>hK' : μ K ≠ ⊤<GOAL>μ (⇑(f a) ⁻¹' s \ K) ≤ ε / 2
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : R1Space X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : BorelSpace Y<VAR>inst✝² : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>hfg : Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasurePreserving (⇑g) μ ν<VAR>this : ν.InnerRegularCompactLTTop<VAR>s : Set Y<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hso : IsOpen s<VAR>hνs' : μ (⇑g ⁻¹' s) ≠ ⊤<VAR>K : Set X<VAR>hKg : MapsTo (⇑g) K s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2<VAR>hKm : MeasurableSet K<VAR>a : α<VAR>hfa : MeasurePreserving (⇑(f a)) μ ν<VAR>ha : MapsTo (⇑(f a)) K s<VAR>hK' : μ K ≠ ⊤<GOAL>μ (⇑g ⁻¹' s \ K) ≤ ε / 2
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp : Pair K<VAR>zeroth_s_eq : g.s.get? 0 = some gp<GOAL>g.conts 1 = { a := gp.b * g.h + gp.a, b := gp.b }
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp : Pair K<VAR>zeroth_s_eq : g.s.get? 0 = some gp<GOAL>g.contsAux 2 = { a := gp.b * g.h + gp.a, b := gp.b }
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g'✝ e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasFDerivWithinAt (fun x => f i x) (f' i) s x<GOAL>HasFDerivWithinAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' (l.get i)).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) s x
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g'✝ e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasFDerivWithinAt (fun x => f i x) (f' i) s x<GOAL>HasFDerivWithinAt (fun x => (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.finRange l.length)).prod) (∑ x_1 : Fin l.length, (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod • (f' (l.get x_1)).smulRight (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod) s x
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g'✝ e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasFDerivWithinAt (fun x => f i x) (f' i) s x<GOAL>(∑ i : Fin l.length, (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.take (↑i) (List.finRange l.length))).prod • (proj i).smulRight (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.drop (↑i).succ (List.finRange l.length))).prod).comp (ContinuousLinearMap.pi fun i => f' (l.get i)) = ∑ x_1 : Fin l.length, (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod • (f' (l.get x_1)).smulRight (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α →ₘ[μ] ℝ≥0∞<GOAL>∫⁻ (a : α), ↑f a ∂μ = f.lintegral
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<GOAL>im I * im z = im z
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<GOAL>∃ f, f.IsSubordinate fun x => (chartAt H x).source
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>x : M<VAR>x✝ : x ∈ univ<GOAL>x ∈ ⋃ i, (chartAt H i).source
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableAt I I' f x<VAR>hxs : UniqueMDiffWithinAt I s x<GOAL>_root_.mfderivWithin I I' f s x = mfderiv I I' f x