[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set X
⊢ ℝ≥0∞
[PROOFSTEP]
borelize X
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ ℝ≥0∞
[PROOFSTEP]
exact ⨆ (d : ℝ≥0) (_ : @hausdorffMeasure X _ _ ⟨rfl⟩ d s = ∞), d
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
⊢ dimH s = ⨆ (d : ℝ≥0) (_ : ↑↑μH[↑d] s = ⊤), ↑d
[PROOFSTEP]
borelize X
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
s : Set X
inst✝ : BorelSpace X
this✝ : MeasurableSpace X := borel X
⊢ dimH s = ⨆ (d : ℝ≥0) (_ : ↑↑μH[↑d] s = ⊤), ↑d
[PROOFSTEP]
rw [dimH]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ↑d < dimH s
⊢ ↑↑μH[↑d] s = ⊤
[PROOFSTEP]
simp only [dimH_def, lt_iSup_iff] at h 
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ∃ i i_1, ↑d < ↑i
⊢ ↑↑μH[↑d] s = ⊤
[PROOFSTEP]
rcases h with ⟨d', hsd', hdd'⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d d' : ℝ≥0
hsd' : ↑↑μH[↑d'] s = ⊤
hdd' : ↑d < ↑d'
⊢ ↑↑μH[↑d] s = ⊤
[PROOFSTEP]
rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hdd' 
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d d' : ℝ≥0
hsd' : ↑↑μH[↑d'] s = ⊤
hdd' : ↑d < ↑d'
⊢ ↑↑μH[↑d] s = ⊤
[PROOFSTEP]
exact top_unique (hsd' ▸ hausdorffMeasure_mono hdd'.le _)
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ↑↑μH[↑d] s = ⊤
⊢ ↑d ≤ dimH s
[PROOFSTEP]
rw [dimH_def]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ↑↑μH[↑d] s = ⊤
⊢ ↑d ≤ ⨆ (d : ℝ≥0) (_ : ↑↑μH[↑d] s = ⊤), ↑d
[PROOFSTEP]
exact le_iSup₂ (α := ℝ≥0∞) d h
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : dimH s < ↑d
⊢ ↑↑μH[↑d] s = 0
[PROOFSTEP]
rw [dimH_def] at h 
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h✝ : dimH s < ↑d
h : ⨆ (d : ℝ≥0) (_ : ↑↑μH[↑d] s = ⊤), ↑d < ↑d
⊢ ↑↑μH[↑d] s = 0
[PROOFSTEP]
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hsd', hd'd⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h✝ : dimH s < ↑d
h : ⨆ (d : ℝ≥0) (_ : ↑↑μH[↑d] s = ⊤), ↑d < ↑d
d' : ℝ≥0
hsd' : ⨆ (d : ℝ≥0) (_ : ↑↑μH[↑d] s = ⊤), ↑d < ↑d'
hd'd : ↑d' < ↑d
⊢ ↑↑μH[↑d] s = 0
[PROOFSTEP]
rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hd'd 
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝³ : EMetricSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h✝ : dimH s < ↑d
h : ⨆ (d : ℝ≥0) (_ : ↑↑μH[↑d] s = ⊤), ↑d < ↑d
d' : ℝ≥0
hsd' : ⨆ (d : ℝ≥0) (_ : ↑↑μH[↑d] s = ⊤), ↑d < ↑d'
hd'd : ↑d' < ↑d
⊢ ↑↑μH[↑d] s = 0
[PROOFSTEP]
exact (hausdorffMeasure_zero_or_top hd'd s).resolve_right fun h₂ => hsd'.not_le <| le_iSup₂ (α := ℝ≥0∞) d' h₂
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s t : Set X
h : s ⊆ t
⊢ dimH s ≤ dimH t
[PROOFSTEP]
borelize X
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s t : Set X
h : s ⊆ t
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s ≤ dimH t
[PROOFSTEP]
exact dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top <| top_unique <| hd ▸ measure_mono h
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set X
h : Set.Subsingleton s
⊢ dimH s = 0
[PROOFSTEP]
borelize X
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set X
h : Set.Subsingleton s
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s = 0
[PROOFSTEP]
apply le_antisymm _ (zero_le _)
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set X
h : Set.Subsingleton s
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s ≤ 0
[PROOFSTEP]
refine dimH_le_of_hausdorffMeasure_ne_top ?_
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set X
h : Set.Subsingleton s
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ ↑↑μH[↑0] s ≠ ⊤
[PROOFSTEP]
exact ((hausdorffMeasure_le_one_of_subsingleton h le_rfl).trans_lt ENNReal.one_lt_top).ne
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : Encodable ι
s : ι → Set X
⊢ dimH (⋃ (i : ι), s i) = ⨆ (i : ι), dimH (s i)
[PROOFSTEP]
borelize X
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : Encodable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH (⋃ (i : ι), s i) = ⨆ (i : ι), dimH (s i)
[PROOFSTEP]
refine le_antisymm (dimH_le fun d hd => ?_) (iSup_le fun i => dimH_mono <| subset_iUnion _ _)
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : Encodable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ↑↑μH[↑d] (⋃ (i : ι), s i) = ⊤
⊢ ↑d ≤ ⨆ (i : ι), dimH (s i)
[PROOFSTEP]
contrapose! hd
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : Encodable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ (i : ι), dimH (s i) < ↑d
⊢ ↑↑μH[↑d] (⋃ (i : ι), s i) ≠ ⊤
[PROOFSTEP]
have : ∀ i, μH[d] (s i) = 0 := fun i => hausdorffMeasure_of_dimH_lt ((le_iSup (fun i => dimH (s i)) i).trans_lt hd)
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : Encodable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ (i : ι), dimH (s i) < ↑d
this : ∀ (i : ι), ↑↑μH[↑d] (s i) = 0
⊢ ↑↑μH[↑d] (⋃ (i : ι), s i) ≠ ⊤
[PROOFSTEP]
rw [measure_iUnion_null this]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : Encodable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ (i : ι), dimH (s i) < ↑d
this : ∀ (i : ι), ↑↑μH[↑d] (s i) = 0
⊢ 0 ≠ ⊤
[PROOFSTEP]
exact ENNReal.zero_ne_top
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set ι
hs : Set.Countable s
t : ι → Set X
⊢ dimH (⋃ (i : ι) (_ : i ∈ s), t i) = ⨆ (i : ι) (_ : i ∈ s), dimH (t i)
[PROOFSTEP]
haveI := hs.toEncodable
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set ι
hs : Set.Countable s
t : ι → Set X
this : Encodable ↑s
⊢ dimH (⋃ (i : ι) (_ : i ∈ s), t i) = ⨆ (i : ι) (_ : i ∈ s), dimH (t i)
[PROOFSTEP]
rw [biUnion_eq_iUnion, dimH_iUnion, ← iSup_subtype'']
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
S : Set (Set X)
hS : Set.Countable S
⊢ dimH (⋃₀ S) = ⨆ (s : Set X) (_ : s ∈ S), dimH s
[PROOFSTEP]
rw [sUnion_eq_biUnion, dimH_bUnion hS]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s t : Set X
⊢ dimH (s ∪ t) = max (dimH s) (dimH t)
[PROOFSTEP]
rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond, ENNReal.sup_eq_max]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set X
hs : Set.Countable s
⊢ dimH (⋃ (x : X) (_ : x ∈ s), {x}) = 0
[PROOFSTEP]
simp only [dimH_bUnion hs, dimH_singleton, ENNReal.iSup_zero_eq_zero]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : r < dimH s
⊢ ∃ x, x ∈ s ∧ ∀ (t : Set X), t ∈ 𝓝[s] x → r < dimH t
[PROOFSTEP]
contrapose! h
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : ∀ (x : X), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ dimH t ≤ r
⊢ dimH s ≤ r
[PROOFSTEP]
choose! t htx htr using h
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : X → Set X
htx : ∀ (x : X), x ∈ s → t x ∈ 𝓝[s] x
htr : ∀ (x : X), x ∈ s → dimH (t x) ≤ r
⊢ dimH s ≤ r
[PROOFSTEP]
rcases countable_cover_nhdsWithin htx with ⟨S, hSs, hSc, hSU⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : X → Set X
htx : ∀ (x : X), x ∈ s → t x ∈ 𝓝[s] x
htr : ∀ (x : X), x ∈ s → dimH (t x) ≤ r
S : Set X
hSs : S ⊆ s
hSc : Set.Countable S
hSU : s ⊆ ⋃ (x : X) (_ : x ∈ S), t x
⊢ dimH s ≤ r
[PROOFSTEP]
calc
  dimH s ≤ dimH (⋃ x ∈ S, t x) := dimH_mono hSU
  _ = ⨆ x ∈ S, dimH (t x) := (dimH_bUnion hSc _)
  _ ≤ r := iSup₂_le fun x hx => htr x <| hSs hx
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ (x : X) (_ : x ∈ s), limsup dimH (smallSets (𝓝[s] x)) = dimH s
[PROOFSTEP]
refine le_antisymm (iSup₂_le fun x _ => ?_) ?_
[GOAL]
case refine_1
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
x : X
x✝ : x ∈ s
⊢ limsup dimH (smallSets (𝓝[s] x)) ≤ dimH s
[PROOFSTEP]
refine limsup_le_of_le isCobounded_le_of_bot ?_
[GOAL]
case refine_1
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
x : X
x✝ : x ∈ s
⊢ ∀ᶠ (n : Set X) in smallSets (𝓝[s] x), dimH n ≤ dimH s
[PROOFSTEP]
exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩
[GOAL]
case refine_2
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
⊢ dimH s ≤ ⨆ (x : X) (_ : x ∈ s), limsup dimH (smallSets (𝓝[s] x))
[PROOFSTEP]
refine le_of_forall_ge_of_dense fun r hr => ?_
[GOAL]
case refine_2
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
⊢ r ≤ ⨆ (x : X) (_ : x ∈ s), limsup dimH (smallSets (𝓝[s] x))
[PROOFSTEP]
rcases exists_mem_nhdsWithin_lt_dimH_of_lt_dimH hr with ⟨x, hxs, hxr⟩
[GOAL]
case refine_2.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ (t : Set X), t ∈ 𝓝[s] x → r < dimH t
⊢ r ≤ ⨆ (x : X) (_ : x ∈ s), limsup dimH (smallSets (𝓝[s] x))
[PROOFSTEP]
refine le_iSup₂_of_le x hxs ?_
[GOAL]
case refine_2.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ (t : Set X), t ∈ 𝓝[s] x → r < dimH t
⊢ r ≤ limsup dimH (smallSets (𝓝[s] x))
[PROOFSTEP]
rw [limsup_eq]
[GOAL]
case refine_2.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ (t : Set X), t ∈ 𝓝[s] x → r < dimH t
⊢ r ≤ sInf {a | ∀ᶠ (n : Set X) in smallSets (𝓝[s] x), dimH n ≤ a}
[PROOFSTEP]
refine le_sInf fun b hb => ?_
[GOAL]
case refine_2.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ (t : Set X), t ∈ 𝓝[s] x → r < dimH t
b : ℝ≥0∞
hb : b ∈ {a | ∀ᶠ (n : Set X) in smallSets (𝓝[s] x), dimH n ≤ a}
⊢ r ≤ b
[PROOFSTEP]
rcases eventually_smallSets.1 hb with ⟨t, htx, ht⟩
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ (t : Set X), t ∈ 𝓝[s] x → r < dimH t
b : ℝ≥0∞
hb : b ∈ {a | ∀ᶠ (n : Set X) in smallSets (𝓝[s] x), dimH n ≤ a}
t : Set X
htx : t ∈ 𝓝[s] x
ht : ∀ (t_1 : Set X), t_1 ⊆ t → dimH t_1 ≤ b
⊢ r ≤ b
[PROOFSTEP]
exact (hxr t htx).le.trans (ht t Subset.rfl)
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ (x : X), limsup dimH (smallSets (𝓝[s] x)) = dimH s
[PROOFSTEP]
refine le_antisymm (iSup_le fun x => ?_) ?_
[GOAL]
case refine_1
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
x : X
⊢ limsup dimH (smallSets (𝓝[s] x)) ≤ dimH s
[PROOFSTEP]
refine limsup_le_of_le isCobounded_le_of_bot ?_
[GOAL]
case refine_1
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
x : X
⊢ ∀ᶠ (n : Set X) in smallSets (𝓝[s] x), dimH n ≤ dimH s
[PROOFSTEP]
exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩
[GOAL]
case refine_2
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
⊢ dimH s ≤ ⨆ (x : X), limsup dimH (smallSets (𝓝[s] x))
[PROOFSTEP]
rw [← bsupr_limsup_dimH]
[GOAL]
case refine_2
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ (x : X) (_ : x ∈ s), limsup dimH (smallSets (𝓝[s] x)) ≤ ⨆ (x : X), limsup dimH (smallSets (𝓝[s] x))
[PROOFSTEP]
exact iSup₂_le_iSup _ _
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
⊢ dimH (f '' s) ≤ dimH s / ↑r
[PROOFSTEP]
borelize X Y
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
⊢ dimH (f '' s) ≤ dimH s / ↑r
[PROOFSTEP]
refine dimH_le fun d hd => ?_
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f '' s) = ⊤
⊢ ↑d ≤ dimH s / ↑r
[PROOFSTEP]
have := h.hausdorffMeasure_image_le hr d.coe_nonneg
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f '' s) = ⊤
this : ↑↑μH[↑d] (f '' s) ≤ ↑C ^ ↑d * ↑↑μH[↑r * ↑d] s
⊢ ↑d ≤ dimH s / ↑r
[PROOFSTEP]
rw [hd, ENNReal.coe_rpow_of_nonneg _ d.coe_nonneg, top_le_iff] at this 
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * ↑↑μH[↑r * ↑d] s = ⊤
⊢ ↑d ≤ dimH s / ↑r
[PROOFSTEP]
have Hrd : μH[(r * d : ℝ≥0)] s = ⊤ := by
  contrapose this
  exact ENNReal.mul_ne_top ENNReal.coe_ne_top this
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * ↑↑μH[↑r * ↑d] s = ⊤
⊢ ↑↑μH[↑(r * d)] s = ⊤
[PROOFSTEP]
contrapose this
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f '' s) = ⊤
this : ¬↑↑μH[↑(r * d)] s = ⊤
⊢ ¬↑(C ^ ↑d) * ↑↑μH[↑r * ↑d] s = ⊤
[PROOFSTEP]
exact ENNReal.mul_ne_top ENNReal.coe_ne_top this
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * ↑↑μH[↑r * ↑d] s = ⊤
Hrd : ↑↑μH[↑(r * d)] s = ⊤
⊢ ↑d ≤ dimH s / ↑r
[PROOFSTEP]
rw [ENNReal.le_div_iff_mul_le, mul_comm, ← ENNReal.coe_mul]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * ↑↑μH[↑r * ↑d] s = ⊤
Hrd : ↑↑μH[↑(r * d)] s = ⊤
⊢ ↑(r * d) ≤ dimH s
case h0
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * ↑↑μH[↑r * ↑d] s = ⊤
Hrd : ↑↑μH[↑(r * d)] s = ⊤
⊢ ↑r ≠ 0 ∨ dimH s ≠ 0
case ht
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f '' s) = ⊤
this : ↑(C ^ ↑d) * ↑↑μH[↑r * ↑d] s = ⊤
Hrd : ↑↑μH[↑(r * d)] s = ⊤
⊢ ↑r ≠ ⊤ ∨ dimH s ≠ ⊤
[PROOFSTEP]
exacts [le_dimH_of_hausdorffMeasure_eq_top Hrd, Or.inl (mt ENNReal.coe_eq_zero.1 hr.ne'), Or.inl ENNReal.coe_ne_top]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C K r✝ : ℝ≥0
f✝ : X → Y
s✝ t : Set X
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
hf : ∀ (x : X), x ∈ s → ∃ C t, t ∈ 𝓝[s] x ∧ HolderOnWith C r f t
⊢ dimH (f '' s) ≤ dimH s / ↑r
[PROOFSTEP]
choose! C t htn hC using hf
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C✝ K r✝ : ℝ≥0
f✝ : X → Y
s✝ t✝ : Set X
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ (x : X), x ∈ s → t x ∈ 𝓝[s] x
hC : ∀ (x : X), x ∈ s → HolderOnWith (C x) r f (t x)
⊢ dimH (f '' s) ≤ dimH s / ↑r
[PROOFSTEP]
rcases countable_cover_nhdsWithin htn with ⟨u, hus, huc, huU⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C✝ K r✝ : ℝ≥0
f✝ : X → Y
s✝ t✝ : Set X
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ (x : X), x ∈ s → t x ∈ 𝓝[s] x
hC : ∀ (x : X), x ∈ s → HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : Set.Countable u
huU : s ⊆ ⋃ (x : X) (_ : x ∈ u), t x
⊢ dimH (f '' s) ≤ dimH s / ↑r
[PROOFSTEP]
replace huU := inter_eq_self_of_subset_left huU
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C✝ K r✝ : ℝ≥0
f✝ : X → Y
s✝ t✝ : Set X
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ (x : X), x ∈ s → t x ∈ 𝓝[s] x
hC : ∀ (x : X), x ∈ s → HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : Set.Countable u
huU : s ∩ ⋃ (x : X) (_ : x ∈ u), t x = s
⊢ dimH (f '' s) ≤ dimH s / ↑r
[PROOFSTEP]
rw [inter_iUnion₂] at huU 
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C✝ K r✝ : ℝ≥0
f✝ : X → Y
s✝ t✝ : Set X
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ (x : X), x ∈ s → t x ∈ 𝓝[s] x
hC : ∀ (x : X), x ∈ s → HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : Set.Countable u
huU : ⋃ (i : X) (_ : i ∈ u), s ∩ t i = s
⊢ dimH (f '' s) ≤ dimH s / ↑r
[PROOFSTEP]
rw [← huU, image_iUnion₂, dimH_bUnion huc, dimH_bUnion huc]
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C✝ K r✝ : ℝ≥0
f✝ : X → Y
s✝ t✝ : Set X
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ (x : X), x ∈ s → t x ∈ 𝓝[s] x
hC : ∀ (x : X), x ∈ s → HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : Set.Countable u
huU : ⋃ (i : X) (_ : i ∈ u), s ∩ t i = s
⊢ ⨆ (i : X) (_ : i ∈ u), dimH (f '' (s ∩ t i)) ≤ (⨆ (i : X) (_ : i ∈ u), dimH (s ∩ t i)) / ↑r
[PROOFSTEP]
simp only [ENNReal.iSup_div]
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C✝ K r✝ : ℝ≥0
f✝ : X → Y
s✝ t✝ : Set X
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ (x : X), x ∈ s → t x ∈ 𝓝[s] x
hC : ∀ (x : X), x ∈ s → HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : Set.Countable u
huU : ⋃ (i : X) (_ : i ∈ u), s ∩ t i = s
⊢ ⨆ (i : X) (_ : i ∈ u), dimH (f '' (s ∩ t i)) ≤ ⨆ (i : X) (_ : i ∈ u), dimH (s ∩ t i) / ↑r
[PROOFSTEP]
exact iSup₂_mono fun x hx => ((hC x (hus hx)).mono (inter_subset_right _ _)).dimH_image_le hr
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C K r✝ : ℝ≥0
f✝ : X → Y
s t : Set X
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C s, s ∈ 𝓝 x ∧ HolderOnWith C r f s
⊢ dimH (range f) ≤ dimH univ / ↑r
[PROOFSTEP]
rw [← image_univ]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C K r✝ : ℝ≥0
f✝ : X → Y
s t : Set X
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C s, s ∈ 𝓝 x ∧ HolderOnWith C r f s
⊢ dimH (f '' univ) ≤ dimH univ / ↑r
[PROOFSTEP]
refine dimH_image_le_of_locally_holder_on hr fun x _ => ?_
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C K r✝ : ℝ≥0
f✝ : X → Y
s t : Set X
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C s, s ∈ 𝓝 x ∧ HolderOnWith C r f s
x : X
x✝ : x ∈ univ
⊢ ∃ C t, t ∈ 𝓝[univ] x ∧ HolderOnWith C r f t
[PROOFSTEP]
simpa only [exists_prop, nhdsWithin_univ] using hf x
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
h : LipschitzOnWith K f s
⊢ dimH (f '' s) ≤ dimH s
[PROOFSTEP]
simpa using h.holderOnWith.dimH_image_le zero_lt_one
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C K r : ℝ≥0
f✝ : X → Y
s✝ t : Set X
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ (x : X), x ∈ s → ∃ C t, t ∈ 𝓝[s] x ∧ LipschitzOnWith C f t
⊢ dimH (f '' s) ≤ dimH s
[PROOFSTEP]
have : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t := by simpa only [holderOnWith_one] using hf
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C K r : ℝ≥0
f✝ : X → Y
s✝ t : Set X
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ (x : X), x ∈ s → ∃ C t, t ∈ 𝓝[s] x ∧ LipschitzOnWith C f t
⊢ ∀ (x : X), x ∈ s → ∃ C t, t ∈ 𝓝[s] x ∧ HolderOnWith C 1 f t
[PROOFSTEP]
simpa only [holderOnWith_one] using hf
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C K r : ℝ≥0
f✝ : X → Y
s✝ t : Set X
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ (x : X), x ∈ s → ∃ C t, t ∈ 𝓝[s] x ∧ LipschitzOnWith C f t
this : ∀ (x : X), x ∈ s → ∃ C t, t ∈ 𝓝[s] x ∧ HolderOnWith C 1 f t
⊢ dimH (f '' s) ≤ dimH s
[PROOFSTEP]
simpa only [ENNReal.coe_one, div_one] using dimH_image_le_of_locally_holder_on zero_lt_one this
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C K r : ℝ≥0
f✝ : X → Y
s t : Set X
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C s, s ∈ 𝓝 x ∧ LipschitzOnWith C f s
⊢ dimH (range f) ≤ dimH univ
[PROOFSTEP]
rw [← image_univ]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C K r : ℝ≥0
f✝ : X → Y
s t : Set X
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C s, s ∈ 𝓝 x ∧ LipschitzOnWith C f s
⊢ dimH (f '' univ) ≤ dimH univ
[PROOFSTEP]
refine dimH_image_le_of_locally_lipschitz_on fun x _ => ?_
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
C K r : ℝ≥0
f✝ : X → Y
s t : Set X
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C s, s ∈ 𝓝 x ∧ LipschitzOnWith C f s
x : X
x✝ : x ∈ univ
⊢ ∃ C t, t ∈ 𝓝[univ] x ∧ LipschitzOnWith C f t
[PROOFSTEP]
simpa only [exists_prop, nhdsWithin_univ] using hf x
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
hf : AntilipschitzWith K f
s : Set Y
⊢ dimH (f ⁻¹' s) ≤ dimH s
[PROOFSTEP]
borelize X Y
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
⊢ dimH (f ⁻¹' s) ≤ dimH s
[PROOFSTEP]
refine dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top ?_
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f ⁻¹' s) = ⊤
⊢ ↑↑μH[↑d] s = ⊤
[PROOFSTEP]
have := hf.hausdorffMeasure_preimage_le d.coe_nonneg s
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f ⁻¹' s) = ⊤
this : ↑↑μH[↑d] (f ⁻¹' s) ≤ ↑K ^ ↑d * ↑↑μH[↑d] s
⊢ ↑↑μH[↑d] s = ⊤
[PROOFSTEP]
rw [hd, top_le_iff] at this 
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f ⁻¹' s) = ⊤
this : ↑K ^ ↑d * ↑↑μH[↑d] s = ⊤
⊢ ↑↑μH[↑d] s = ⊤
[PROOFSTEP]
contrapose! this
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f ⁻¹' s) = ⊤
this : ↑↑μH[↑d] s ≠ ⊤
⊢ ↑K ^ ↑d * ↑↑μH[↑d] s ≠ ⊤
[PROOFSTEP]
exact ENNReal.mul_ne_top (by simp) this
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : ↑↑μH[↑d] (f ⁻¹' s) = ⊤
this : ↑↑μH[↑d] s ≠ ⊤
⊢ ↑K ^ ↑d ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
e : X ≃ᵢ Y
s : Set Y
⊢ dimH (↑e ⁻¹' s) = dimH s
[PROOFSTEP]
rw [← e.image_symm, e.symm.dimH_image]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
e : X ≃ᵢ Y
⊢ dimH univ = dimH univ
[PROOFSTEP]
rw [← e.dimH_preimage univ, preimage_univ]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : EMetricSpace X
inst✝⁵ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set E
⊢ dimH s ≤ dimH (↑e '' s)
[PROOFSTEP]
simpa only [e.symm_image_image] using e.symm.lipschitz.dimH_image_le (e '' s)
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : EMetricSpace X
inst✝⁵ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set F
⊢ dimH (↑e ⁻¹' s) = dimH s
[PROOFSTEP]
rw [← e.image_symm_eq_preimage, e.symm.dimH_image]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : EMetricSpace X
inst✝⁵ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
⊢ dimH univ = dimH univ
[PROOFSTEP]
rw [← e.dimH_preimage, preimage_univ]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
⊢ dimH (Metric.ball x r) = ↑(Fintype.card ι)
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ dimH (Metric.ball x r) = ↑(Fintype.card ι)
[PROOFSTEP]
rwa [dimH_subsingleton, eq_comm, Nat.cast_eq_zero, Fintype.card_eq_zero_iff]
[GOAL]
case inl
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ Set.Subsingleton (Metric.ball x r)
[PROOFSTEP]
exact fun x _ y _ => Subsingleton.elim x y
[GOAL]
case inr
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ dimH (Metric.ball x r) = ↑(Fintype.card ι)
[PROOFSTEP]
rw [← ENNReal.coe_nat]
[GOAL]
case inr
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ dimH (Metric.ball x r) = ↑↑(Fintype.card ι)
[PROOFSTEP]
have : μH[Fintype.card ι] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) := by
  rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr, rpow_nat_cast]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ ↑↑μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ ↑(Fintype.card ι))
[PROOFSTEP]
rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr, rpow_nat_cast]
[GOAL]
case inr
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : ↑↑μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ ↑(Fintype.card ι))
⊢ dimH (Metric.ball x r) = ↑↑(Fintype.card ι)
[PROOFSTEP]
refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_
[GOAL]
case inr.refine_1
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : ↑↑μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ ↑(Fintype.card ι))
⊢ ↑↑μH[↑↑(Fintype.card ι)] (Metric.ball x r) ≠ 0
[PROOFSTEP]
rw [NNReal.coe_nat_cast, this]
[GOAL]
case inr.refine_2
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : ↑↑μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ ↑(Fintype.card ι))
⊢ ↑↑μH[↑↑(Fintype.card ι)] (Metric.ball x r) ≠ ⊤
[PROOFSTEP]
rw [NNReal.coe_nat_cast, this]
[GOAL]
case inr.refine_1
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : ↑↑μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ ↑(Fintype.card ι))
⊢ ENNReal.ofReal ((2 * r) ^ ↑(Fintype.card ι)) ≠ 0
[PROOFSTEP]
simp [pow_pos (mul_pos (zero_lt_two' ℝ) hr)]
[GOAL]
case inr.refine_2
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : ↑↑μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ ↑(Fintype.card ι))
⊢ ENNReal.ofReal ((2 * r) ^ ↑(Fintype.card ι)) ≠ ⊤
[PROOFSTEP]
exact ENNReal.ofReal_ne_top
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
x : Fin n → ℝ
r : ℝ
hr : 0 < r
⊢ dimH (Metric.ball x r) = ↑n
[PROOFSTEP]
rw [dimH_ball_pi x hr, Fintype.card_fin]
[GOAL]
ι✝ : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : EMetricSpace X
inst✝⁵ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝⁴ : Fintype ι✝
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_5
inst✝ : Fintype ι
⊢ dimH univ = ↑(Fintype.card ι)
[PROOFSTEP]
simp only [← Metric.iUnion_ball_nat_succ (0 : ι → ℝ), dimH_iUnion, dimH_ball_pi _ (Nat.cast_add_one_pos _), iSup_const]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
⊢ dimH univ = ↑n
[PROOFSTEP]
rw [dimH_univ_pi, Fintype.card_fin]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ dimH s = ↑(finrank ℝ E)
[PROOFSTEP]
have e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq (FiniteDimensional.finrank_fin_fun ℝ).symm
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH s = ↑(finrank ℝ E)
[PROOFSTEP]
rw [← e.dimH_image]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH (↑e '' s) = ↑(finrank ℝ E)
[PROOFSTEP]
refine le_antisymm ?_ ?_
[GOAL]
case refine_1
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH (↑e '' s) ≤ ↑(finrank ℝ E)
[PROOFSTEP]
exact (dimH_mono (subset_univ _)).trans_eq (dimH_univ_pi_fin _)
[GOAL]
case refine_2
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ ↑(finrank ℝ E) ≤ dimH (↑e '' s)
[PROOFSTEP]
have : e '' s ∈ 𝓝 (e x) := by rw [← e.map_nhds_eq]; exact image_mem_map h
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ ↑e '' s ∈ 𝓝 (↑e x)
[PROOFSTEP]
rw [← e.map_nhds_eq]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ ↑e '' s ∈ Filter.map (↑e) (𝓝 x)
[PROOFSTEP]
exact image_mem_map h
[GOAL]
case refine_2
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this : ↑e '' s ∈ 𝓝 (↑e x)
⊢ ↑(finrank ℝ E) ≤ dimH (↑e '' s)
[PROOFSTEP]
rcases Metric.nhds_basis_ball.mem_iff.1 this with ⟨r, hr0, hr⟩
[GOAL]
case refine_2.intro.intro
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r✝ : ℝ≥0
f : X → Y
s✝ t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this : ↑e '' s ∈ 𝓝 (↑e x)
r : ℝ
hr0 : 0 < r
hr : Metric.ball (↑e x) r ⊆ ↑e '' s
⊢ ↑(finrank ℝ E) ≤ dimH (↑e '' s)
[PROOFSTEP]
simpa only [dimH_ball_pi_fin (e x) hr0] using dimH_mono hr
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s t : Set X
E : Type u_4
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ dimH univ = 1
[PROOFSTEP]
rw [dimH_univ_eq_finrank ℝ, FiniteDimensional.finrank_self, Nat.cast_one]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : EMetricSpace X
inst✝⁵ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t : Set X
E : Type u_4
F : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
hs : dimH s < ↑(finrank ℝ E)
⊢ Dense sᶜ
[PROOFSTEP]
refine fun x => mem_closure_iff_nhds.2 fun t ht => nonempty_iff_ne_empty.2 fun he => hs.not_le ?_
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : EMetricSpace X
inst✝⁵ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t✝ : Set X
E : Type u_4
F : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ∩ sᶜ = ∅
⊢ ↑(finrank ℝ E) ≤ dimH s
[PROOFSTEP]
rw [← diff_eq, diff_eq_empty] at he 
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : EMetricSpace X
inst✝⁵ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t✝ : Set X
E : Type u_4
F : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ⊆ s
⊢ ↑(finrank ℝ E) ≤ dimH s
[PROOFSTEP]
rw [← Real.dimH_of_mem_nhds ht]
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : EMetricSpace X
inst✝⁵ : EMetricSpace Y
C K r : ℝ≥0
f : X → Y
s✝ t✝ : Set X
E : Type u_4
F : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ⊆ s
⊢ dimH t ≤ dimH s
[PROOFSTEP]
exact dimH_mono he
[GOAL]
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : EMetricSpace X
inst✝⁵ : EMetricSpace Y
C K r : ℝ≥0
f✝ : X → Y
s t : Set X
E : Type u_4
F : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h : ContDiff ℝ 1 f
⊢ dimH (range f) = dimH (f '' univ)
[PROOFSTEP]
rw [image_univ]
