internlm/Lean-Github huggingface dataset:
Theorem: LocalVolume.closure_interior
Proof state before:
case intro.intro.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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
es : ball y t ⊆ s ∩ ball x r
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
exact lt_of_lt_of_le (bp y t (by bound)) (measure_mono es)
Proof state after:
no goals
Theorem: LocalVolume.closure_interior
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ s ∩ ball x r
Tactic:
simp only [Set.subset_inter_iff]
Proof state after:
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ s ∧ ball y t ⊆ ball x r
Theorem: LocalVolume.closure_interior
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ s ∧ ball y t ⊆ ball x r
Tactic:
constructor
Proof state after:
case left
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ s

case right
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ ball x r
Theorem: LocalVolume.closure_interior
Proof state before:
case left
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ s

case right
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ ball x r
Tactic:
exact _root_.trans (Metric.ball_subset_ball (by bound)) (_root_.trans ye interior_subset)
Proof state after:
case right
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ ball x r
Theorem: LocalVolume.closure_interior
Proof state before:
case right
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ ball x r
Tactic:
apply Metric.ball_subset_ball'
Proof state after:
case right.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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ t + dist y x ≤ r
Theorem: LocalVolume.closure_interior
Proof state before:
case right.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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ t + dist y x ≤ r
Tactic:
trans r - dist x y + dist y x
Proof state after:
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ t + dist y x ≤ r - dist x y + dist y x

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ r - dist x y + dist y x ≤ r
Theorem: LocalVolume.closure_interior
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ t + dist y x ≤ r - dist x y + dist y x

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ r - dist x y + dist y x ≤ r
Tactic:
bound
Proof state after:
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ r - dist x y + dist y x ≤ r
Theorem: LocalVolume.closure_interior
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ r - dist x y + dist y x ≤ r
Tactic:
simp [dist_comm]
Proof state after:
no goals
Theorem: LocalVolume.closure_interior
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ t ≤ e
Tactic:
bound
Proof state after:
no goals
Theorem: LocalVolume.closure_interior
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
es : ball y t ⊆ s ∩ ball x r
⊢ t > 0
Tactic:
bound
Proof state after:
no goals
Theorem: LocalVolume.Ioc
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
a b : ℝ
⊢ LocalVolumeSet (Set.Ioc a b)
Tactic:
apply LocalVolume.closure_interior
Proof state after:
case bp
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
a b : ℝ
⊢ ∀ (x r : ℝ), r > 0 → ↑volume (ball x r) > 0

case ci
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
a b : ℝ
⊢ Set.Ioc a b ⊆ closure (interior (Set.Ioc a b))
Theorem: LocalVolume.Ioc
Proof state before:
case bp
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
a b : ℝ
⊢ ∀ (x r : ℝ), r > 0 → ↑volume (ball x r) > 0
Tactic:
intro x r rp
Proof state after:
case bp
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
a b x r : ℝ
rp : r > 0
⊢ ↑volume (ball x r) > 0
Theorem: LocalVolume.Ioc
Proof state before:
case bp
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
a b x r : ℝ
rp : r > 0
⊢ ↑volume (ball x r) > 0
Tactic:
simp only [Real.volume_ball, gt_iff_lt, ENNReal.ofReal_pos, mul_pos_iff_of_pos_left,
  zero_lt_bit0, zero_lt_one]
Proof state after:
case bp
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
a b x r : ℝ
rp : r > 0
⊢ 0 < 2 * r
Theorem: LocalVolume.Ioc
Proof state before:
case bp
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
a b x r : ℝ
rp : r > 0
⊢ 0 < 2 * r
Tactic:
bound
Proof state after:
no goals
Theorem: LocalVolume.Ioc
Proof state before:
case ci
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
a b : ℝ
⊢ Set.Ioc a b ⊆ closure (interior (Set.Ioc a b))
Tactic:
by_cases ab : a = b
Proof state after:
case pos
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
a b : ℝ
ab : a = b
⊢ Set.Ioc a b ⊆ closure (interior (Set.Ioc a b))

case neg
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
a b : ℝ
ab : ¬a = b
⊢ Set.Ioc a b ⊆ closure (interior (Set.Ioc a b))
Theorem: LocalVolume.Ioc
Proof state before:
case neg
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
a b : ℝ
ab : ¬a = b
⊢ Set.Ioc a b ⊆ closure (interior (Set.Ioc a b))
Tactic:
simp only [interior_Ioc, closure_Ioo ab, Set.Ioc_subset_Icc_self]
Proof state after:
no goals
Theorem: LocalVolume.Ioc
Proof state before:
case pos
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
a b : ℝ
ab : a = b
⊢ Set.Ioc a b ⊆ closure (interior (Set.Ioc a b))
Tactic:
simp only [ab, Set.Ioc_self, Set.empty_subset]
Proof state after:
no goals
Theorem: mean_squeeze
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 → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
lo : b ≤ ⨍ (x : X) in s, f x
hi : ∀ x ∈ s, f x ≤ b
⊢ ∀ x ∈ s, f x = b
Tactic:
contrapose lo
Proof state after:
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
lo : ¬∀ x ∈ s, f x = b
⊢ ¬b ≤ ⨍ (x : X) in s, f x