internlm/Lean-Github huggingface dataset:
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
hcovering : K n ⊆ ⋃ x, U x
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
let ⟨v, hv⟩ := IsCompact.elim_finite_subcover (hcompact n) U hUopen hcovering
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
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
⊢ ↑μ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
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
have hnull: ∀ i : v, μH[d] (f '' (s ∩ U i)) = 0 := by
  intro i
  have h₂ : μH[d] (s ∩ U i) = 0 := measure_mono_null (inter_subset_left s (U ↑i)) hs
  have h₁ := ((hfL i).mono (hut i)).mono (inter_subset_right s (U i))
  refine lipschitz_image_null_set_is_null_set (Nat.cast_nonneg d) h₁ 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
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
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
⊢ ↑μ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
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
have coe : ⋃ (i : v), U i = ⋃ (i : X) (_ : i ∈ v), U i := iUnion_coe_set _ _
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
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ ↑μ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
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
rw [← coe] at hv
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
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ ↑μ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
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
have : f '' (s ∩ (K n)) ⊆ ⋃ (i : v), f '' (s ∩ (U i)) := by
  calc f '' (s ∩ (K n))
    _ ⊆ f '' (s ∩ (⋃ (i : v), U i)) := by
      apply image_subset
      apply inter_subset_inter_right s hv
    _ = f '' ((⋃ (i : v), s ∩ (U i))) := by rw [inter_iUnion]
    _ = ⋃ (i : v), f '' ( s ∩ (U i)) := image_iUnion
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
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
⊢ ↑μ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
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
have hless : μH[d] (f '' (s ∩ (K n))) ≤ 0 := by
  calc μH[d] (f '' (s ∩ (K n)))
    _ ≤ μH[d] (⋃ (i : v), f '' (s ∩ (U i))) := measure_mono this
    _ ≤ ∑' (i : v), (μH[d] (f '' (s ∩ (U i))) : ℝ≥0∞) := by apply measure_iUnion_le
    _ = ∑' (_ : v), (0 : ℝ≥0∞) := tsum_congr hnull
    _ = 0 := by simp
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
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
hless : ↑μH[↑d] (f '' (s ∩ K n)) ≤ 0
⊢ ↑μ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
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
hless : ↑μH[↑d] (f '' (s ∩ K n)) ≤ 0
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
simp only [nonpos_iff_eq_zero, zero_le] at hless ⊢
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
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
hless : ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ ↑μ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
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i, U ↑i
hnull : ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
coe : ⋃ i, U ↑i = ⋃ i ∈ v, U i
this : f '' (s ∩ K n) ⊆ ⋃ i, f '' (s ∩ U ↑i)
hless : ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ ↑μH[↑d] (f '' (s ∩ K n)) = 0
Tactic:
exact hless
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
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
apply null_set_from_countable_cover _ _ ass
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)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ f '' s ⊆ ⋃ n, f '' (s ∩ K n)
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)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ f '' s ⊆ ⋃ n, f '' (s ∩ K n)
Tactic:
rw [← image_iUnion]
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)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ f '' s ⊆ f '' ⋃ i, s ∩ K i
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)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ f '' s ⊆ f '' ⋃ i, s ∩ K i
Tactic:
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
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)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
this : s = ⋃ n, s ∩ K n
⊢ f '' s ⊆ f '' ⋃ i, s ∩ K i
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)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
this : s = ⋃ n, s ∩ K n
⊢ f '' s ⊆ f '' ⋃ i, s ∩ K i
Tactic:
exact Eq.subset (congrArg (image f) this)
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
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ s = ⋃ n, s ∩ K n
Tactic:
calc s
_ = s ∩ univ := (inter_univ s).symm
_ = s ∩ ⋃ (n : ℕ), K n := by rw [hcov]
_ = ⋃ (n : ℕ), s ∩ K n := by apply inter_iUnion s
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
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ s ∩ univ = s ∩ ⋃ n, K n
Tactic:
rw [hcov]
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
K : ℕ → Set X := compactCovering X
hcov : ⋃ n, K n = univ
hcompact : ∀ (n : ℕ), IsCompact (K n)
ass : ∀ (n : ℕ), ↑μH[↑d] (f '' (s ∩ K n)) = 0
⊢ s ∩ ⋃ n, K n = ⋃ n, s ∩ K n
Tactic:
apply inter_iUnion s
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
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
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
⊢ ∀ (i : { x // x ∈ v }), ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
Tactic:
intro i
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
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 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
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
Tactic:
have h₂ : μH[d] (s ∩ U i) = 0 := measure_mono_null (inter_subset_left s (U ↑i)) hs
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
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
h₂ : ↑μH[↑d] (s ∩ U ↑i) = 0
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 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
hcovering : K n ⊆ ⋃ x, U x
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
h₂ : ↑μH[↑d] (s ∩ U ↑i) = 0
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0
Tactic:
have h₁ := ((hfL i).mono (hut i)).mono (inter_subset_right s (U i))
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
v : Finset X
hv : K n ⊆ ⋃ i ∈ v, U i
i : { x // x ∈ v }
h₂ : ↑μH[↑d] (s ∩ U ↑i) = 0
h₁ : LipschitzOnWith (Kx ↑i) f (s ∩ U ↑i)
⊢ ↑μH[↑d] (f '' (s ∩ U ↑i)) = 0