ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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 μ ∧ HasCompactSupport 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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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 μ ∧ HasCompactSupport 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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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 μ ∧ HasCompactSupport 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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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_compact : IsCompact s<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 μ ∧ HasCompactSupport 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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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_compact : IsCompact s<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 μ ∧ HasCompactSupport 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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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_compact : IsCompact s<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 μ ∧ HasCompactSupport 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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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_compact : IsCompact s<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>k : Set α<VAR>k_compact : IsCompact k<VAR>sk : s ⊆ interior k<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ HasCompactSupport 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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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_compact : IsCompact s<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>k : Set α<VAR>k_compact : IsCompact k<VAR>sk : s ⊆ interior k<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_support : Function.support f ⊆ interior k<VAR>f_mem : Memℒp f p μ<GOAL>∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ HasCompactSupport 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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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_compact : IsCompact s<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>k : Set α<VAR>k_compact : IsCompact k<VAR>sk : s ⊆ interior k<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_support : Function.support f ⊆ interior k<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 μ ∧ HasCompactSupport 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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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_compact : IsCompact s<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>k : Set α<VAR>k_compact : IsCompact k<VAR>sk : s ⊆ interior k<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_support : Function.support f ⊆ interior k<VAR>f_mem : Memℒp f p μ<VAR>I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε<VAR>x : α<VAR>hx : x ∉ k<GOAL>f x = 0
<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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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_compact : IsCompact s<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>k : Set α<VAR>k_compact : IsCompact k<VAR>sk : s ⊆ interior k<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_support : Function.support f ⊆ interior k<VAR>f_mem : Memℒp f p μ<VAR>I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε<VAR>x : α<VAR>hx : x ∉ k<GOAL>x ∉ Function.support 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✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<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_compact : IsCompact s<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>k : Set α<VAR>k_compact : IsCompact k<VAR>sk : s ⊆ interior k<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_support : Function.support f ⊆ interior k<VAR>f_mem : Memℒp f p μ<VAR>I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε<VAR>x : α<VAR>hx : x ∈ Function.support f<GOAL>x ∈ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>hb : ¬IsMax b<GOAL>Ioo a (succ b) = Ioc a b
<VAR>x✝ y x : ℂ<VAR>hx : cos x ≠ 0<GOAL>(1 + tan x ^ 2)⁻¹ = cos x ^ 2
<VAR>x✝ y x : ℂ<VAR>hx : cos x ≠ 0<GOAL>(1 + sin x ^ 2 / cos x ^ 2)⁻¹ = cos x ^ 2
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)<VAR>M : HomologicalComplex C c<VAR>α : M ⟶ K<VAR>β : M ⟶ L<VAR>i : ι<GOAL>(biprod.lift α β).f i ≫ biprod.fst.f i = α.f i
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>f : Arrow C<VAR>inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>S : SplitEpi f.hom<VAR>n : ℕ<GOAL>WidePullback.lift (WidePullback.base fun x => f.hom) (fun i => if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_ else WidePullback.π (fun x => f.hom) (i.pred x)) ⋯ ≫ WidePullback.π (fun x => f.hom) 0 = (WidePullback.base fun x => f.hom) ≫ S.section_
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>f : Arrow C<VAR>inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>S : SplitEpi f.hom<VAR>n : ℕ<GOAL>(if h : True then (WidePullback.base fun x => f.hom) ≫ S.section_ else WidePullback.π (fun x => f.hom) (Fin.pred 0 ⋯)) = (WidePullback.base fun x => f.hom) ≫ S.section_
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>a : ↥A<GOAL>of ↑(φ a) = t * of ↑a * t⁻¹
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>a : ↥A<GOAL>of ↑(φ a) = of ↑(φ a) * t * t⁻¹
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedAddCommGroup Y<VAR>inst✝³ : NormedAddCommGroup Z<VAR>inst✝² : NormedSpace ℝ X<VAR>inst✝¹ : NormedSpace ℝ Y<VAR>inst✝ : NormedSpace ℝ Z<VAR>f : X → Y<VAR>g : Y → Z<VAR>x : X<VAR>f' : X →L[ℝ] Y<VAR>hf₁ : HasFDerivAt f f' x<VAR>cf : IsConformalMap f'<VAR>g' : Y →L[ℝ] Z<VAR>hg₁ : HasFDerivAt g g' (f x)<VAR>cg : IsConformalMap g'<GOAL>ConformalAt (g ∘ f) x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<GOAL>(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ∈ corootSpace ⇑α
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<VAR>e : L<VAR>he₀ : e ≠ 0<VAR>he : ∀ (x : ↥H), ⁅x, e⁆ = α x • e<GOAL>(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ∈ corootSpace ⇑α
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<VAR>e : L<VAR>he₀ : e ≠ 0<VAR>he : ∀ (x : ↥H), ⁅x, e⁆ = α x • e<VAR>heα : e ∈ rootSpace H ⇑α<GOAL>(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ∈ corootSpace ⇑α
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<VAR>e : L<VAR>he₀ : e ≠ 0<VAR>he : ∀ (x : ↥H), ⁅x, e⁆ = α x • e<VAR>heα : e ∈ rootSpace H ⇑α<VAR>f : L<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>hf : ((killingForm K L) e) f ≠ 0<GOAL>(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ∈ corootSpace ⇑α
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<VAR>e : L<VAR>he₀ : e ≠ 0<VAR>he : ∀ (x : ↥H), ⁅x, e⁆ = α x • e<VAR>heα : e ∈ rootSpace H ⇑α<VAR>f : L<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>hf : ((killingForm K L) e) f ≠ 0<GOAL>⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
<VAR>o : Ordinal.{u_1}<VAR>ho : 0 < o<GOAL>0 < aleph' o
<VAR>T : Type u<VAR>inst✝¹ : Category.{v, u} T<VAR>f g : Arrow T<VAR>sq : f ⟶ g<VAR>inst✝ : IsIso sq<GOAL>sq.left ≫ g.hom ≫ inv sq.right = f.hom
<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>hn : x ≠ y<VAR>h : ‖x‖ = ‖y‖<GOAL>o.oangle y x = ↑π - 2 • o.oangle (y - x) y
<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>hn : x ≠ y<VAR>h : ‖x‖ = ‖y‖<GOAL>o.oangle y x = ↑π - (o.oangle (y - x) y + o.oangle (y - x) y)
<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>hn : x ≠ y<VAR>h : ‖x‖ = ‖y‖<GOAL>o.oangle y x = ↑π - (o.oangle x (x - y) + o.oangle (y - x) y)
<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>hn : x ≠ y<VAR>h : ‖x‖ = ‖y‖<GOAL>o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = ↑π
<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>hn : x ≠ y<VAR>h : ‖x‖ = ‖y‖<VAR>hy : y ≠ 0<GOAL>o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = ↑π
<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>hn : x ≠ y<VAR>h : ‖x‖ = ‖y‖<VAR>hy : y ≠ 0<VAR>hx : x ≠ 0<GOAL>o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = ↑π
<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>hn : x ≠ y<VAR>h : ‖x‖ = ‖y‖<VAR>hy : y ≠ 0<VAR>hx : x ≠ 0<GOAL>o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = o.oangle (-y) (-x) + o.oangle x (-(y - x)) + o.oangle (y - x) (- -y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a✝ : α<VAR>b : β<VAR>a x : α<VAR>y : β<GOAL>(x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := ⋯ } t
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : AffineSpace V P<VAR>inst✝³ : Ring k<VAR>inst✝² : Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>b₂ : AffineBasis ι k P<VAR>inst✝ : DecidableEq ι<VAR>l m : ι<GOAL>(b.coords (b₂ l) ᵥ* b₂.toMatrix ⇑b) m = 1 l m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>T R n = 2 * X * T R (n - 1) - T R (n - 2)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>inst✝ : ProperSpace E<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>a b : E<GOAL>Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>hf : Function.Surjective ⇑f<GOAL>AffineSubspace.map f ⊤ = ⊤
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>hf : Function.Surjective ⇑f<GOAL>↑(AffineSubspace.map f ⊤) = ↑⊤
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<GOAL>Measure.map X ℙ = ProbabilityTheory.cond μ (toMeasurable μ s) ↔ Measure.map X ℙ = ProbabilityTheory.cond μ s