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

case neg
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
by_cases hs₀ : s ⊆ Ioi 0
case neg.intro.intro
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : ¬δ ∈ Ioi 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
case neg
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
obtain ⟨δ, hδs, δ_nonpos⟩ := not_subset.mp hs₀
case neg.intro.intro
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
case neg.intro.intro
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : ¬δ ∈ Ioi 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
rw [Set.mem_Ioi, not_lt] at δ_nonpos
case neg.intro.intro.h₁
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure E ⊆ ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E

case neg.intro.intro.h₂
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ (⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E) ⊆ closure E
case neg.intro.intro
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
apply Subset.antisymm
case pos
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : s ⊆ Ioi 0
⊢ cthickening 0 E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
case pos
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : s ⊆ Ioi 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
rw [← cthickening_zero]
no goals
case pos
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : s ⊆ Ioi 0
⊢ cthickening 0 E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
apply cthickening_eq_iInter_cthickening' _ hs₀ hs
no goals
case neg.intro.intro.h₁
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure E ⊆ ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
exact subset_iInter₂ fun ε _ => closure_subset_cthickening ε E
case neg.intro.intro.h₂
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ (⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E) ⊆ cthickening δ E
case neg.intro.intro.h₂
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ (⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E) ⊆ closure E
rw [← cthickening_of_nonpos δ_nonpos E]
no goals
case neg.intro.intro.h₂
ι : Sort ?u.143633
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ (⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E) ⊆ cthickening δ E
exact biInter_subset_of_mem hδs