internlm/Lean-Github huggingface dataset:
Theorem: extendedChart_differential_bijective
Proof state before:
case refine_2.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
H : Type u_2
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
inst✝⁸ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
s : M
hs : s ∈ e.source
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source
Tactic:
have : (e.extend I).symm (e.extend I s) = s := e.extend_left_inv _ hs
Proof state after:
case refine_2.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
H : Type u_2
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
inst✝⁸ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source
Theorem: extendedChart_differential_bijective
Proof state before:
case refine_2.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
H : Type u_2
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
inst✝⁸ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ ↑(e.extend I).symm (↑(e.extend I) s) ∈ e.source
Tactic:
rw [this]
Proof state after:
case refine_2.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
H : Type u_2
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
inst✝⁸ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ s ∈ e.source
Theorem: extendedChart_differential_bijective
Proof state before:
case refine_2.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
H : Type u_2
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
inst✝⁸ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
s : M
hs : s ∈ e.source
this : ↑(e.extend I).symm (↑(e.extend I) s) = s
⊢ s ∈ e.source
Tactic:
exact hs
Proof state after:
no goals
Theorem: extendedChart_differential_bijective
Proof state before:
case refine_3
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
H : Type u_2
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
inst✝⁸ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
⊢ ∀ x ∈ e.source, ↑(e.extend I).symm (↑(e.extend I) x) = x
Tactic:
exact fun x hx ↦ e.extend_left_inv I hx
Proof state after:
no goals
Theorem: extendedChart_differential_bijective
Proof state before:
case refine_4
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
H : Type u_2
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
inst✝⁸ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
⊢ ∀ y ∈ ↑(e.extend I) '' e.source, ↑(e.extend I) (↑(e.extend I).symm y) = y
Tactic:
exact fun x hx ↦ e.extend_right_inv _ hx
Proof state after:
no goals
Theorem: extendedChart_differential_bijective
Proof state before:
case refine_5
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
H : Type u_2
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
inst✝⁸ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
G : Type u_5
inst✝⁵ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
inst✝² : SmoothManifoldWithCorners J N
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
he : e ∈ atlas H M
x : M
hx : x ∈ e.source
diff : ContMDiffOn 𝓘(ℝ, E) I 1 (↑(e.extend I).symm) (↑(e.extend I) '' e.source)
⊢ ContMDiffOn I 𝓘(ℝ, E) (↑1) (↑(e.extend I)) e.source
Tactic:
exact SmoothOn.contMDiffOn (extendedChart_smooth I he)
Proof state after:
no goals
Theorem: null_set_from_countable_cover
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
⊢ ↑μ t = 0
Tactic:
have h : μ t ≤ 0 := by
  have : ∀ n, μ (s n ∩ t) = 0 := fun n => measure_inter_null_of_null_left t (hnull n)
  calc μ t
    _ = μ ((⋃ (n : ℕ), s n) ∩ t) := by simp only [inter_eq_right.mpr hcov]
    _ = μ (⋃ (n : ℕ), (s n ∩ t)) := by rw [iUnion_inter]
    _ ≤ ∑' (n : ℕ), μ (s n ∩ t) := by apply OuterMeasure.iUnion_nat
    _ = ∑' (n : ℕ), 0 := by simp_rw [this]
    _ = 0 := by rw [tsum_zero]
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
h : ↑μ t ≤ 0
⊢ ↑μ t = 0
Theorem: null_set_from_countable_cover
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
h : ↑μ t ≤ 0
⊢ ↑μ t = 0
Tactic:
simp only [nonpos_iff_eq_zero, zero_le] at h ⊢
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
h : ↑μ t = 0
⊢ ↑μ t = 0
Theorem: null_set_from_countable_cover
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
h : ↑μ t = 0
⊢ ↑μ t = 0
Tactic:
exact h
Proof state after:
no goals
Theorem: null_set_from_countable_cover
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
⊢ ↑μ t ≤ 0
Tactic:
have : ∀ n, μ (s n ∩ t) = 0 := fun n => measure_inter_null_of_null_left t (hnull n)
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ↑μ t ≤ 0
Theorem: null_set_from_countable_cover
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ↑μ t ≤ 0
Tactic:
calc μ t
  _ = μ ((⋃ (n : ℕ), s n) ∩ t) := by simp only [inter_eq_right.mpr hcov]
  _ = μ (⋃ (n : ℕ), (s n ∩ t)) := by rw [iUnion_inter]
  _ ≤ ∑' (n : ℕ), μ (s n ∩ t) := by apply OuterMeasure.iUnion_nat
  _ = ∑' (n : ℕ), 0 := by simp_rw [this]
  _ = 0 := by rw [tsum_zero]
Proof state after:
no goals
Theorem: null_set_from_countable_cover
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ↑μ t = ↑μ ((⋃ n, s n) ∩ t)
Tactic:
simp only [inter_eq_right.mpr hcov]
Proof state after:
no goals
Theorem: null_set_from_countable_cover
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ↑μ ((⋃ n, s n) ∩ t) = ↑μ (⋃ n, s n ∩ t)
Tactic:
rw [iUnion_inter]
Proof state after:
no goals
Theorem: null_set_from_countable_cover
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ↑μ (⋃ n, s n ∩ t) ≤ ∑' (n : ℕ), ↑μ (s n ∩ t)
Tactic:
apply OuterMeasure.iUnion_nat
Proof state after:
no goals
Theorem: null_set_from_countable_cover
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ∑' (n : ℕ), ↑μ (s n ∩ t) = ∑' (n : ℕ), 0
Tactic:
simp_rw [this]
Proof state after:
no goals
Theorem: null_set_from_countable_cover
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ∑' (n : ℕ), 0 = 0
Tactic:
rw [tsum_zero]
Proof state after:
no goals
Theorem: lipschitz_image_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
⊢ ↑μH[d] (f '' s) = 0
Tactic:
have aux : μH[d] (f '' s) ≤ (K : ENNReal) ^ d * μH[d] s := hf.hausdorffMeasure_image_le hd
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) ≤ ↑K ^ d * ↑μH[d] s
⊢ ↑μH[d] (f '' s) = 0
Theorem: lipschitz_image_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) ≤ ↑K ^ d * ↑μH[d] s
⊢ ↑μH[d] (f '' s) = 0
Tactic:
rw [hs] at aux
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) ≤ ↑K ^ d * 0
⊢ ↑μH[d] (f '' s) = 0
Theorem: lipschitz_image_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) ≤ ↑K ^ d * 0
⊢ ↑μH[d] (f '' s) = 0
Tactic:
simp only [mul_zero, nonpos_iff_eq_zero, hs] at aux ⊢
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) = 0
⊢ ↑μH[d] (f '' s) = 0
Theorem: lipschitz_image_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) = 0
⊢ ↑μH[d] (f '' s) = 0
Tactic:
exact aux
Proof state after:
no goals
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
let K : ℕ → Set X := compactCovering X
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
⊢ ↑μH[↑d] (f '' s) = 0
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
have hcov : ⋃ (n : ℕ), K n = univ := iUnion_compactCovering X
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
⊢ ↑μH[↑d] (f '' s) = 0
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
have hcompact : ∀ n : ℕ, IsCompact (K n) := isCompact_compactCovering X
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
⊢ ↑μH[↑d] (f '' s) = 0
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
suffices ass : ∀ n : ℕ, μH[d] (f '' (s ∩ K n)) = 0 by
  apply null_set_from_countable_cover _ _ ass
  rw [← image_iUnion]
  have : s = ⋃ (n : ℕ), s ∩ K n := by calc s
      _ = s ∩ univ := (inter_univ s).symm
      _ = s ∩ ⋃ (n : ℕ), K n := by rw [hcov]
      _ = ⋃ (n : ℕ), s ∩ K n := by apply inter_iUnion s
  exact Eq.subset (congrArg (image f) this)
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
⊢ ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
⊢ ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
intro n
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
choose Kx t ht hfL using fun x ↦ (hf x)
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
choose U hut hUopen hxU using fun x ↦ mem_nhds_iff.mp (ht x)
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Theorem: locally_lipschitz_image_of_null_set_is_null_set
Proof state before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
have hcovering : K n ⊆ ⋃ (x : X), U x := fun y _ ↦ mem_iUnion_of_mem y (hxU y)
Proof state after:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
hf : LocallyLipschitz f
s : Set X
hs : ↑μH[↑d] s = 0
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
n : ℕ
Kx : X → ℝ≥0
t : X → Set X
ht : ∀ (x : X), t x ∈ 𝓝 x
hfL : ∀ (x : X), LipschitzOnWith (Kx x) f (t x)
U : X → Set X
hut : ∀ (x : X), U x ⊆ t x
hUopen : ∀ (x : X), IsOpen (U x)
hxU : ∀ (x : X), x ∈ U x
hcovering : K n ⊆ ⋃ x, U x
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0