case h₁
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ cthickening δ E ⊆ ⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E

case h₂
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ (⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E) ⊆ cthickening δ E
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E
apply Subset.antisymm
no goals
case h₁
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ cthickening δ E ⊆ ⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E
exact subset_iInter₂ fun _ hε => cthickening_mono (le_of_lt (hsδ hε)) E
case h₂
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ (⋂ (ε : ℝ) (_ : ε ∈ s), {x | infEdist x E ≤ ENNReal.ofReal ε}) ⊆ {x | infEdist x E ≤ ENNReal.ofReal δ}
case h₂
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ (⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E) ⊆ cthickening δ E
unfold cthickening
case h₂
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : x ∈ ⋂ (ε : ℝ) (_ : ε ∈ s), {x | infEdist x E ≤ ENNReal.ofReal ε}
⊢ x ∈ {x | infEdist x E ≤ ENNReal.ofReal δ}
case h₂
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ (⋂ (ε : ℝ) (_ : ε ∈ s), {x | infEdist x E ≤ ENNReal.ofReal ε}) ⊆ {x | infEdist x E ≤ ENNReal.ofReal δ}
intro x hx
case h₂
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
⊢ infEdist x E ≤ ENNReal.ofReal δ
case h₂
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : x ∈ ⋂ (ε : ℝ) (_ : ε ∈ s), {x | infEdist x E ≤ ENNReal.ofReal ε}
⊢ x ∈ {x | infEdist x E ≤ ENNReal.ofReal δ}
simp only [mem_iInter, mem_setOf_eq] at *
case h₂.h
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
⊢ ∀ (ε : ℝ≥0), 0 < ε → ENNReal.ofReal δ < ⊤ → infEdist x E ≤ ENNReal.ofReal δ + ↑ε
case h₂
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
⊢ infEdist x E ≤ ENNReal.ofReal δ
apply ENNReal.le_of_forall_pos_le_add
case h₂.h
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
⊢ infEdist x E ≤ ENNReal.ofReal δ + ↑η
case h₂.h
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
⊢ ∀ (ε : ℝ≥0), 0 < ε → ENNReal.ofReal δ < ⊤ → infEdist x E ≤ ENNReal.ofReal δ + ↑ε
intro η η_pos _
case h₂.h.intro.intro
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ infEdist x E ≤ ENNReal.ofReal δ + ↑η
case h₂.h
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
⊢ infEdist x E ≤ ENNReal.ofReal δ + ↑η
rcases hs (δ + η) (lt_add_of_pos_right _ (NNReal.coe_pos.mpr η_pos)) with ⟨ε, ⟨hsε, hε⟩⟩
case h₂.h.intro.intro
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ ENNReal.ofReal (δ + ↑η) ≤ ENNReal.ofReal δ + ↑η
case h₂.h.intro.intro
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ infEdist x E ≤ ENNReal.ofReal δ + ↑η
apply ((hx ε hsε).trans (ENNReal.ofReal_le_ofReal hε.2)).trans
case h₂.h.intro.intro
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ ENNReal.ofReal (δ + ↑η) ≤ ENNReal.ofReal δ + ENNReal.ofReal ↑η
case h₂.h.intro.intro
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ ENNReal.ofReal (δ + ↑η) ≤ ENNReal.ofReal δ + ↑η
rw [ENNReal.coe_nnreal_eq η]
no goals
case h₂.h.intro.intro
ι : Sort ?u.139615
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ ENNReal.ofReal (δ + ↑η) ≤ ENNReal.ofReal δ + ENNReal.ofReal ↑η
exact ENNReal.ofReal_add_le