internlm/Lean-Github huggingface dataset:
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.hF_meas.h.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
y : X
ys : y ∈ s
t : ℝ
ts : t ∈ Ioc a b
⊢ (fun t => (y, t)) t ∈ s ×ˢ Icc a b
Tactic:
exact Set.mk_mem_prod ys (Set.Ioc_subset_Icc_self ts)
Proof state after:
no goals
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_bound
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (t : ℝ) ∂volume, t ∈ Ι a b → ‖f x t‖ ≤ c
Tactic:
apply eventually_nhdsWithin_of_forall
Proof state after:
case intro.intro.h_bound.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ ∀ x ∈ s, ∀ᵐ (t : ℝ) ∂volume, t ∈ Ι a b → ‖f x t‖ ≤ c
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_bound.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ ∀ x ∈ s, ∀ᵐ (t : ℝ) ∂volume, t ∈ Ι a b → ‖f x t‖ ≤ c
Tactic:
intro y ys
Proof state after:
case intro.intro.h_bound.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
y : X
ys : y ∈ s
⊢ ∀ᵐ (t : ℝ) ∂volume, t ∈ Ι a b → ‖f y t‖ ≤ c
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_bound.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
y : X
ys : y ∈ s
⊢ ∀ᵐ (t : ℝ) ∂volume, t ∈ Ι a b → ‖f y t‖ ≤ c
Tactic:
rw [Set.uIoc_of_le ab]
Proof state after:
case intro.intro.h_bound.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
y : X
ys : y ∈ s
⊢ ∀ᵐ (t : ℝ) ∂volume, t ∈ Ioc a b → ‖f y t‖ ≤ c
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_bound.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
y : X
ys : y ∈ s
⊢ ∀ᵐ (t : ℝ) ∂volume, t ∈ Ioc a b → ‖f y t‖ ≤ c
Tactic:
apply ae_of_all
Proof state after:
case intro.intro.h_bound.h.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
y : X
ys : y ∈ s
⊢ ∀ a_1 ∈ Ioc a b, ‖f y a_1‖ ≤ c
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_bound.h.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
y : X
ys : y ∈ s
⊢ ∀ a_1 ∈ Ioc a b, ‖f y a_1‖ ≤ c
Tactic:
intro t ts
Proof state after:
case intro.intro.h_bound.h.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
y : X
ys : y ∈ s
t : ℝ
ts : t ∈ Ioc a b
⊢ ‖f y t‖ ≤ c
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_bound.h.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
y : X
ys : y ∈ s
t : ℝ
ts : t ∈ Ioc a b
⊢ ‖f y t‖ ≤ c
Tactic:
apply fb _ ys _ (Set.Ioc_subset_Icc_self ts)
Proof state after:
no goals
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.bound_integrable
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ IntervalIntegrable (fun x => c) volume a b
Tactic:
exact intervalIntegrable_const
Proof state after:
no goals
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_cont
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ ∀ᵐ (t : ℝ) ∂volume, t ∈ Ι a b → ContinuousWithinAt (fun x => f x t) s x
Tactic:
apply ae_of_all
Proof state after:
case intro.intro.h_cont.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ ∀ a_1 ∈ Ι a b, ContinuousWithinAt (fun x => f x a_1) s x
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_cont.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ ∀ a_1 ∈ Ι a b, ContinuousWithinAt (fun x => f x a_1) s x
Tactic:
intro t ts
Proof state after:
case intro.intro.h_cont.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ ContinuousWithinAt (fun x => f x t) s x
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_cont.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ ContinuousWithinAt (fun x => f x t) s x
Tactic:
simp_rw [e]
Proof state after:
case intro.intro.h_cont.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ ContinuousWithinAt (fun x => uncurry f (x, t)) s x
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_cont.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ ContinuousWithinAt (fun x => uncurry f (x, t)) s x
Tactic:
apply fc.comp
Proof state after:
case intro.intro.h_cont.a.hf
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ ContinuousOn (fun x => (x, t)) s

case intro.intro.h_cont.a.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ Set.MapsTo (fun x => (x, t)) s (s ×ˢ Icc a b)

case intro.intro.h_cont.a.a
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ x ∈ s
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_cont.a.hf
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ ContinuousOn (fun x => (x, t)) s
Tactic:
apply Continuous.continuousOn
Proof state after:
case intro.intro.h_cont.a.hf.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ Continuous fun x => (x, t)
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_cont.a.hf.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ Continuous fun x => (x, t)
Tactic:
exact Continuous.Prod.mk_left t
Proof state after:
no goals
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_cont.a.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ Set.MapsTo (fun x => (x, t)) s (s ×ˢ Icc a b)
Tactic:
rw [Set.uIoc_of_le ab] at ts
Proof state after:
case intro.intro.h_cont.a.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ioc a b
⊢ Set.MapsTo (fun x => (x, t)) s (s ×ˢ Icc a b)
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_cont.a.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ioc a b
⊢ Set.MapsTo (fun x => (x, t)) s (s ×ˢ Icc a b)
Tactic:
intro y ys
Proof state after:
case intro.intro.h_cont.a.h
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ioc a b
y : X
ys : y ∈ s
⊢ (fun x => (x, t)) y ∈ s ×ˢ Icc a b