Theorem: ContinuousOn.intervalIntegral (Ray/Misc/Measure.lean)

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⟩
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

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
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

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
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

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]
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

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
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

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)
x : X
xs : x ∈ s
⊢ ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..b, f x t) s x
Tactic:
apply intervalIntegral.continuousWithinAt_of_dominated_interval (bound := fun _ ↦ c)
State after:
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))

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

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

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

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]
State after:
no goals

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
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))

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
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))

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
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)

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]
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)

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]
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)

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
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)

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
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)

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
State after:
no goals

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
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

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)
State after:
no goals

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
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

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
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

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]
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

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
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

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
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

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)
State after:
no goals

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
State after:
no goals

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
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

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
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

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]
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

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
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

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
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)

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
State after:
no goals

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
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)

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
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

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
y : X
ys : y ∈ s
⊢ (fun x => (x, t)) y ∈ s ×ˢ Icc a b
Tactic:
exact Set.mk_mem_prod ys (Set.Ioc_subset_Icc_self ts)
State after:
no goals

State before:
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
Tactic:
assumption
State after:
no goals