internlm/Lean-Github huggingface dataset:
Theorem: mean_squeeze
Proof state before:
case intro.intro.intro.intro.hfs
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 → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) (s \ t) volume
Tactic:
exact fi.mono (Set.diff_subset _ _) (le_refl _)
Proof state after:
no goals
Theorem: mean_squeeze
Proof state before:
case intro.intro.intro.intro.hft
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 → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) t volume
Tactic:
exact fi.mono ts (le_refl _)
Proof state after:
no goals
Theorem: ContinuousOn.intervalIntegral
Proof state before:
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
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..b, f x t) s
Tactic:
rcases ((sc.prod isCompact_Icc).bddAbove_image fc.norm).exists_ge 0 with ⟨c, _, fb⟩
Proof state after:
case intro.intro
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 : ∀ y ∈ (fun x => ‖uncurry f x‖) '' s ×ˢ Icc a b, y ≤ c
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..b, f x t) s
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro
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 : ∀ y ∈ (fun x => ‖uncurry f x‖) '' s ×ˢ Icc a b, y ≤ c
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..b, f x t) s
Tactic:
simp only [Set.forall_mem_image] at fb
Proof state after:
case intro.intro
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 : X × ℝ⦄, x ∈ s ×ˢ Icc a b → ‖uncurry f x‖ ≤ c
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..b, f x t) s
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro
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 : X × ℝ⦄, x ∈ s ×ˢ Icc a b → ‖uncurry f x‖ ≤ c
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..b, f x t) s
Tactic:
simp only [Set.forall_prod_set, uncurry] at fb
Proof state after:
case intro.intro
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
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..b, f x t) s
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro
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
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..b, f x t) s
Tactic:
have e : ∀ x t, f x t = (uncurry f) (x, t) := by
  simp only [Function.uncurry_apply_pair, eq_self_iff_true, forall_const, imp_true_iff]
Proof state after:
case intro.intro
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)
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..b, f x t) s
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro
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)
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..b, f x t) s
Tactic:
intro x xs
Proof state after:
case intro.intro
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
⊢ ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..b, f x t) s x
Theorem: ContinuousOn.intervalIntegral
Proof state before:
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
⊢ ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
Tactic:
simp only [Function.uncurry_apply_pair, eq_self_iff_true, forall_const, imp_true_iff]
Proof state after:
no goals
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.hF_meas
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, AEStronglyMeasurable (fun t => f x t) (volume.restrict (Ι a b))
Tactic:
apply eventually_nhdsWithin_of_forall
Proof state after:
case intro.intro.hF_meas.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, AEStronglyMeasurable (fun t => f x t) (volume.restrict (Ι a b))
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.hF_meas.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, AEStronglyMeasurable (fun t => f x t) (volume.restrict (Ι a b))
Tactic:
intro y ys
Proof state after:
case intro.intro.hF_meas.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
⊢ AEStronglyMeasurable (fun t => f y t) (volume.restrict (Ι a b))
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.hF_meas.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
⊢ AEStronglyMeasurable (fun t => f y t) (volume.restrict (Ι a b))
Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioc
Proof state after:
case intro.intro.hF_meas.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
⊢ ContinuousOn (fun t => f y t) (Ι a b)
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.hF_meas.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
⊢ ContinuousOn (fun t => f y t) (Ι a b)
Tactic:
rw [Set.uIoc_of_le ab]
Proof state after:
case intro.intro.hF_meas.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
⊢ ContinuousOn (fun t => f y t) (Ioc a b)
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.hF_meas.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
⊢ ContinuousOn (fun t => f y t) (Ioc a b)
Tactic:
simp_rw [e]
Proof state after:
case intro.intro.hF_meas.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
⊢ ContinuousOn (fun t => uncurry f (y, t)) (Ioc a b)
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.hF_meas.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
⊢ ContinuousOn (fun t => uncurry f (y, t)) (Ioc a b)
Tactic:
apply fc.comp
Proof state after:
case intro.intro.hF_meas.h.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
y : X
ys : y ∈ s
⊢ ContinuousOn (fun t => (y, t)) (Ioc a b)

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
⊢ Set.MapsTo (fun t => (y, t)) (Ioc a b) (s ×ˢ Icc a b)
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.hF_meas.h.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
y : X
ys : y ∈ s
⊢ ContinuousOn (fun t => (y, t)) (Ioc a b)
Tactic:
apply Continuous.continuousOn
Proof state after:
case intro.intro.hF_meas.h.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
y : X
ys : y ∈ s
⊢ Continuous fun t => (y, t)
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.hF_meas.h.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
y : X
ys : y ∈ s
⊢ Continuous fun t => (y, t)
Tactic:
exact Continuous.Prod.mk y
Proof state after:
no goals
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
⊢ Set.MapsTo (fun t => (y, t)) (Ioc a b) (s ×ˢ Icc a b)
Tactic:
intro t ts
Proof state after:
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