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


[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
[PROOFSTEP]
have := x.property.some_mem
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : Set.Nonempty.some (_ : ↑x ∈ (inducedMap A).fst) ∈ ⋂ (n : ℕ), A (res (↑x) n)
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
[PROOFSTEP]
rw [mem_iInter] at this
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : ∀ (i : ℕ), Set.Nonempty.some (_ : ↑x ∈ (inducedMap A).fst) ∈ A (res (↑x) i)
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
[PROOFSTEP]
exact this n
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
⊢ Injective (inducedMap A).snd
[PROOFSTEP]
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
[GOAL]
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
[PROOFSTEP]
refine' Subtype.coe_injective (res_injective _)
[GOAL]
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res ((fun a => ↑a) { val := x, property := hx }) = res ((fun a => ↑a) { val := y, property := hy })
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res x = res y
[PROOFSTEP]
ext n : 1
[GOAL]
case mk.mk.h
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
⊢ res x n = res y n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case mk.mk.h.zero
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res x Nat.zero = res y Nat.zero
[PROOFSTEP]
simp
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ res x (Nat.succ n) = res y (Nat.succ n)
[PROOFSTEP]
simp only [res_succ, cons.injEq]
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ x n = y n ∧ res x n = res y n
[PROOFSTEP]
refine' ⟨_, ih⟩
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ x n = y n
[PROOFSTEP]
contrapose hA
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ¬CantorScheme.Disjoint A
[PROOFSTEP]
simp only [CantorScheme.Disjoint, _root_.Pairwise, Ne.def, not_forall, exists_prop]
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ∃ x x_1 x_2, ¬x_1 = x_2 ∧ ¬_root_.Disjoint (A (x_1 :: x)) (A (x_2 :: x))
[PROOFSTEP]
refine' ⟨res x n, _, _, hA, _⟩
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ¬_root_.Disjoint (A (x n :: res x n)) (A (y n :: res x n))
[PROOFSTEP]
rw [not_disjoint_iff]
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ∃ x_1, x_1 ∈ A (x n :: res x n) ∧ x_1 ∈ A (y n :: res x n)
[PROOFSTEP]
refine' ⟨(inducedMap A).2 ⟨x, hx⟩, _, _⟩
[GOAL]
case mk.mk.h.succ.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (x n :: res x n)
[PROOFSTEP]
rw [← res_succ]
[GOAL]
case mk.mk.h.succ.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (res x (Nat.succ n))
[PROOFSTEP]
apply map_mem
[GOAL]
case mk.mk.h.succ.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (y n :: res x n)
[PROOFSTEP]
rw [hxy, ih, ← res_succ]
[GOAL]
case mk.mk.h.succ.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := y, property := hy } ∈ A (res y (Nat.succ n))
[PROOFSTEP]
apply map_mem
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
hA : VanishingDiam A
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
[PROOFSTEP]
specialize hA x
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : Tendsto (fun n => EMetric.diam (A (res x n))) atTop (𝓝 0)
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
[PROOFSTEP]
rw [ENNReal.tendsto_atTop_zero] at hA
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
[PROOFSTEP]
cases'
  hA (ENNReal.ofReal (ε / 2))
    (by
      simp only [gt_iff_lt, ENNReal.ofReal_pos]
      linarith) with
  n hn
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ ENNReal.ofReal (ε / 2) > 0
[PROOFSTEP]
simp only [gt_iff_lt, ENNReal.ofReal_pos]
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ 0 < ε / 2
[PROOFSTEP]
linarith
[GOAL]
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
[PROOFSTEP]
use n
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
[PROOFSTEP]
intro y hy z hz
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ dist y z < ε
[PROOFSTEP]
rw [← ENNReal.ofReal_lt_ofReal_iff ε_pos, ← edist_dist]
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ edist y z < ENNReal.ofReal ε
[PROOFSTEP]
apply lt_of_le_of_lt (EMetric.edist_le_diam_of_mem hy hz)
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ EMetric.diam (A (res x n)) < ENNReal.ofReal ε
[PROOFSTEP]
apply lt_of_le_of_lt (hn _ (le_refl _))
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ ENNReal.ofReal (ε / 2) < ENNReal.ofReal ε
[PROOFSTEP]
rw [ENNReal.ofReal_lt_ofReal_iff ε_pos]
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ ε / 2 < ε
[PROOFSTEP]
linarith
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
⊢ Continuous (inducedMap A).snd
[PROOFSTEP]
rw [Metric.continuous_iff']
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
⊢ ∀ (a : ↑(inducedMap A).fst) (ε : ℝ),
    ε > 0 → ∀ᶠ (x : ↑(inducedMap A).fst) in 𝓝 a, dist (Sigma.snd (inducedMap A) x) (Sigma.snd (inducedMap A) a) < ε
[PROOFSTEP]
rintro ⟨x, hx⟩ ε ε_pos
[GOAL]
case mk
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
⊢ ∀ᶠ (x_1 : ↑(inducedMap A).fst) in 𝓝 { val := x, property := hx },
    dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε
[PROOFSTEP]
cases' hA.dist_lt _ ε_pos x with n hn
[GOAL]
case mk.intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∀ᶠ (x_1 : ↑(inducedMap A).fst) in 𝓝 { val := x, property := hx },
    dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε
[PROOFSTEP]
rw [_root_.eventually_nhds_iff]
[GOAL]
case mk.intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∃ t,
    (∀ (x_1 : ↑(inducedMap A).fst),
        x_1 ∈ t → dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε) ∧
      IsOpen t ∧ { val := x, property := hx } ∈ t
[PROOFSTEP]
refine' ⟨(↑) ⁻¹' cylinder x n, _, _, by simp⟩
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' cylinder x n
[PROOFSTEP]
simp
[GOAL]
case mk.intro.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∀ (x_1 : ↑(inducedMap A).fst),
    x_1 ∈ Subtype.val ⁻¹' cylinder x n →
      dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε
[PROOFSTEP]
rintro ⟨y, hy⟩ hyx
[GOAL]
case mk.intro.refine'_1.mk
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : { val := y, property := hy } ∈ Subtype.val ⁻¹' cylinder x n
⊢ dist (Sigma.snd (inducedMap A) { val := y, property := hy }) (Sigma.snd (inducedMap A) { val := x, property := hx }) <
    ε
[PROOFSTEP]
rw [mem_preimage, Subtype.coe_mk, cylinder_eq_res, mem_setOf] at hyx
[GOAL]
case mk.intro.refine'_1.mk
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ dist (Sigma.snd (inducedMap A) { val := y, property := hy }) (Sigma.snd (inducedMap A) { val := x, property := hx }) <
    ε
[PROOFSTEP]
apply hn
[GOAL]
case mk.intro.refine'_1.mk.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ Sigma.snd (inducedMap A) { val := y, property := hy } ∈ A (res x n)
[PROOFSTEP]
rw [← hyx]
[GOAL]
case mk.intro.refine'_1.mk.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ Sigma.snd (inducedMap A) { val := y, property := hy } ∈ A (res y n)
[PROOFSTEP]
apply map_mem
[GOAL]
case mk.intro.refine'_1.mk.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (res x n)
[PROOFSTEP]
apply map_mem
[GOAL]
case mk.intro.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ IsOpen (Subtype.val ⁻¹' cylinder x n)
[PROOFSTEP]
apply continuous_subtype_val.isOpen_preimage
[GOAL]
case mk.intro.refine'_2.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ IsOpen (cylinder x n)
[PROOFSTEP]
apply isOpen_cylinder
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
⊢ (inducedMap A).fst = univ
[PROOFSTEP]
rw [eq_univ_iff_forall]
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
⊢ ∀ (x : ℕ → β), x ∈ (inducedMap A).fst
[PROOFSTEP]
intro x
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
⊢ x ∈ (inducedMap A).fst
[PROOFSTEP]
choose u hu using fun n => hnonempty (res x n)
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ x ∈ (inducedMap A).fst
[PROOFSTEP]
have umem : ∀ n m : ℕ, n ≤ m → u m ∈ A (res x n) :=
  by
  have : Antitone fun n : ℕ => A (res x n) :=
    by
    refine' antitone_nat_of_succ_le _
    intro n
    apply hanti.antitone
  intro n m hnm
  exact this hnm (hu _)
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
[PROOFSTEP]
have : Antitone fun n : ℕ => A (res x n) :=
  by
  refine' antitone_nat_of_succ_le _
  intro n
  apply hanti.antitone
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ Antitone fun n => A (res x n)
[PROOFSTEP]
refine' antitone_nat_of_succ_le _
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ ∀ (n : ℕ), A (res x (n + 1)) ≤ A (res x n)
[PROOFSTEP]
intro n
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
n : ℕ
⊢ A (res x (n + 1)) ≤ A (res x n)
[PROOFSTEP]
apply hanti.antitone
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
this : Antitone fun n => A (res x n)
⊢ ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
[PROOFSTEP]
intro n m hnm
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
this : Antitone fun n => A (res x n)
n m : ℕ
hnm : n ≤ m
⊢ u m ∈ A (res x n)
[PROOFSTEP]
exact this hnm (hu _)
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ x ∈ (inducedMap A).fst
[PROOFSTEP]
have : CauchySeq u := by
  rw [Metric.cauchySeq_iff]
  intro ε ε_pos
  cases' hdiam.dist_lt _ ε_pos x with n hn
  use n
  intro m₀ hm₀ m₁ hm₁
  apply hn <;> apply umem <;> assumption
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ CauchySeq u
[PROOFSTEP]
rw [Metric.cauchySeq_iff]
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → dist (u m) (u n) < ε
[PROOFSTEP]
intro ε ε_pos
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → dist (u m) (u n) < ε
[PROOFSTEP]
cases' hdiam.dist_lt _ ε_pos x with n hn
[GOAL]
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → dist (u m) (u n) < ε
[PROOFSTEP]
use n
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∀ (m : ℕ), m ≥ n → ∀ (n_1 : ℕ), n_1 ≥ n → dist (u m) (u n_1) < ε
[PROOFSTEP]
intro m₀ hm₀ m₁ hm₁
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ dist (u m₀) (u m₁) < ε
[PROOFSTEP]
apply hn
[GOAL]
case h.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ u m₀ ∈ A (res x n)
[PROOFSTEP]
apply umem
[GOAL]
case h.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ u m₁ ∈ A (res x n)
[PROOFSTEP]
apply umem
[GOAL]
case h.x.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ n ≤ m₀
[PROOFSTEP]
assumption
[GOAL]
case h.x.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ n ≤ m₁
[PROOFSTEP]
assumption
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
⊢ x ∈ (inducedMap A).fst
[PROOFSTEP]
cases' cauchySeq_tendsto_of_complete this with y hy
[GOAL]
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ x ∈ (inducedMap A).fst
[PROOFSTEP]
use y
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ y ∈ ⋂ (n : ℕ), A (res x n)
[PROOFSTEP]
rw [mem_iInter]
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ ∀ (i : ℕ), y ∈ A (res x i)
[PROOFSTEP]
intro n
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ y ∈ A (res x n)
[PROOFSTEP]
apply hanti _ (x n)
[GOAL]
case h.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ y ∈ closure (A (x n :: res x n))
[PROOFSTEP]
apply mem_closure_of_tendsto hy
[GOAL]
case h.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ ∀ᶠ (x_1 : ℕ) in atTop, u x_1 ∈ A (x n :: res x n)
[PROOFSTEP]
rw [eventually_atTop]
[GOAL]
case h.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → u b ∈ A (x n :: res x n)
[PROOFSTEP]
exact ⟨n.succ, umem _⟩