[GOAL]
X : Type u_1
s : Set X
⊢ (some '' s)ᶜ = some '' sᶜ ∪ {∞}
[PROOFSTEP]
rw [coe_injective.compl_image_eq, compl_range_coe]
[GOAL]
X : Type u_1
x : OnePoint X
⊢ x ≠ ∞ ↔ ∃ y, ↑y = x
[PROOFSTEP]
induction x using OnePoint.rec
[GOAL]
case h₁
X : Type u_1
⊢ ∞ ≠ ∞ ↔ ∃ y, ↑y = ∞
[PROOFSTEP]
simp
[GOAL]
case h₂
X : Type u_1
x✝ : X
⊢ ↑x✝ ≠ ∞ ↔ ∃ y, ↑y = ↑x✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
x : OnePoint X
⊢ ¬x ∈ range some ↔ x = ∞
[PROOFSTEP]
rw [← mem_compl_iff, compl_range_coe, mem_singleton_iff]
[GOAL]
X : Type u_1
⊢ some ⁻¹' {∞} = ∅
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
x✝ : X
⊢ x✝ ∈ some ⁻¹' {∞} ↔ x✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) univ
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
⊢ (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) s →
    (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t →
      (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) (s ∩ t)
[PROOFSTEP]
rintro ⟨hms, hs⟩ ⟨hmt, ht⟩
[GOAL]
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen (some ⁻¹' t)
⊢ (∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ) ∧ IsOpen (some ⁻¹' (s ∩ t))
[PROOFSTEP]
refine' ⟨_, hs.inter ht⟩
[GOAL]
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen (some ⁻¹' t)
⊢ ∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ
[PROOFSTEP]
rintro ⟨hms', hmt'⟩
[GOAL]
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen (some ⁻¹' t)
hms' : ∞ ∈ s
hmt' : ∞ ∈ t
⊢ IsCompact (some ⁻¹' (s ∩ t))ᶜ
[PROOFSTEP]
simpa [compl_inter] using (hms hms').union (hmt hmt')
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
⊢ (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) (⋃₀ S)
[PROOFSTEP]
suffices IsOpen ((↑) ⁻¹' ⋃₀ S : Set X) by
  refine' ⟨_, this⟩
  rintro ⟨s, hsS : s ∈ S, hs : ∞ ∈ s⟩
  refine' isCompact_of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl _
  exact compl_subset_compl.mpr (preimage_mono <| subset_sUnion_of_mem hsS)
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
this : IsOpen (some ⁻¹' ⋃₀ S)
⊢ (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) (⋃₀ S)
[PROOFSTEP]
refine' ⟨_, this⟩
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
this : IsOpen (some ⁻¹' ⋃₀ S)
⊢ ∞ ∈ ⋃₀ S → IsCompact (some ⁻¹' ⋃₀ S)ᶜ
[PROOFSTEP]
rintro ⟨s, hsS : s ∈ S, hs : ∞ ∈ s⟩
[GOAL]
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
this : IsOpen (some ⁻¹' ⋃₀ S)
s : Set (OnePoint X)
hsS : s ∈ S
hs : ∞ ∈ s
⊢ IsCompact (some ⁻¹' ⋃₀ S)ᶜ
[PROOFSTEP]
refine' isCompact_of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl _
[GOAL]
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
this : IsOpen (some ⁻¹' ⋃₀ S)
s : Set (OnePoint X)
hsS : s ∈ S
hs : ∞ ∈ s
⊢ (some ⁻¹' ⋃₀ S)ᶜ ⊆ (some ⁻¹' s)ᶜ
[PROOFSTEP]
exact compl_subset_compl.mpr (preimage_mono <| subset_sUnion_of_mem hsS)
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
⊢ IsOpen (some ⁻¹' ⋃₀ S)
[PROOFSTEP]
rw [preimage_sUnion]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
⊢ IsOpen (⋃ (t : Set (OnePoint X)) (_ : t ∈ S), some ⁻¹' t)
[PROOFSTEP]
exact isOpen_biUnion fun s hs => (ho s hs).2
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
⊢ IsOpen s ↔ IsCompact (some ⁻¹' s)ᶜ ∧ IsOpen (some ⁻¹' s)
[PROOFSTEP]
simp [isOpen_def, h]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
⊢ IsOpen s ↔ IsClosed (some ⁻¹' s)ᶜ ∧ IsCompact (some ⁻¹' s)ᶜ
[PROOFSTEP]
simp only [isOpen_iff_of_mem' h, isClosed_compl_iff, and_comm]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ¬∞ ∈ s
⊢ IsOpen s ↔ IsOpen (some ⁻¹' s)
[PROOFSTEP]
simp [isOpen_def, h]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s)
[PROOFSTEP]
have : ∞ ∉ sᶜ := fun H => H h
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
this : ¬∞ ∈ sᶜ
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s)
[PROOFSTEP]
rw [← isOpen_compl_iff, isOpen_iff_of_not_mem this, ← isOpen_compl_iff, preimage_compl]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ¬∞ ∈ s
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
[PROOFSTEP]
rw [← isOpen_compl_iff, isOpen_iff_of_mem (mem_compl h), ← preimage_compl, compl_compl]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ IsOpen (some '' s) ↔ IsOpen s
[PROOFSTEP]
rw [isOpen_iff_of_not_mem infty_not_mem_image_coe, preimage_image_eq _ coe_injective]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ IsOpen (some '' s)ᶜ ↔ IsClosed s ∧ IsCompact s
[PROOFSTEP]
rw [isOpen_iff_of_mem, ← preimage_compl, compl_compl, preimage_image_eq _ coe_injective]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ ∞ ∈ (some '' s)ᶜ
[PROOFSTEP]
exact infty_not_mem_image_coe
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ IsClosed (some '' s) ↔ IsClosed s ∧ IsCompact s
[PROOFSTEP]
rw [← isOpen_compl_iff, isOpen_compl_image_coe]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ IsClosed {∞}
[PROOFSTEP]
rw [← compl_range_coe, isClosed_compl_iff]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ IsOpen (range some)
[PROOFSTEP]
exact isOpen_range_coe
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x : X
h : NeBot (𝓝[{x}ᶜ] x)
⊢ NeBot (𝓝[{↑x}ᶜ] ↑x)
[PROOFSTEP]
simpa [nhdsWithin_coe, preimage, coe_eq_coe] using h.map some
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ 𝓝[{∞}ᶜ] ∞ = map some (coclosedCompact X)
[PROOFSTEP]
refine' (nhdsWithin_basis_open ∞ _).ext (hasBasis_coclosedCompact.map _) _ _
[GOAL]
case refine'_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ ∀ (i : Set (OnePoint X)), ∞ ∈ i ∧ IsOpen i → ∃ i', (IsClosed i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ
[PROOFSTEP]
rintro s ⟨hs, hso⟩
[GOAL]
case refine'_1.intro
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t : Set X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen s
⊢ ∃ i', (IsClosed i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ s ∩ {∞}ᶜ
[PROOFSTEP]
refine' ⟨_, (isOpen_iff_of_mem hs).mp hso, _⟩
[GOAL]
case refine'_1.intro
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t : Set X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen s
⊢ some '' (some ⁻¹' s)ᶜᶜ ⊆ s ∩ {∞}ᶜ
[PROOFSTEP]
simp [Subset.rfl]
[GOAL]
case refine'_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ ∀ (i' : Set X), IsClosed i' ∧ IsCompact i' → ∃ i, (∞ ∈ i ∧ IsOpen i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ
[PROOFSTEP]
rintro s ⟨h₁, h₂⟩
[GOAL]
case refine'_2.intro
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
h₁ : IsClosed s
h₂ : IsCompact s
⊢ ∃ i, (∞ ∈ i ∧ IsOpen i) ∧ i ∩ {∞}ᶜ ⊆ some '' sᶜ
[PROOFSTEP]
refine' ⟨_, ⟨mem_compl infty_not_mem_image_coe, isOpen_compl_image_coe.2 ⟨h₁, h₂⟩⟩, _⟩
[GOAL]
case refine'_2.intro
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
h₁ : IsClosed s
h₂ : IsCompact s
⊢ (some '' s)ᶜ ∩ {∞}ᶜ ⊆ some '' sᶜ
[PROOFSTEP]
simp [compl_image_coe, ← diff_eq, subset_preimage_image]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : NoncompactSpace X
⊢ NeBot (𝓝[{∞}ᶜ] ∞)
[PROOFSTEP]
rw [nhdsWithin_compl_infty_eq]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : NoncompactSpace X
⊢ NeBot (map some (coclosedCompact X))
[PROOFSTEP]
infer_instance
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ 𝓝 ∞ = map some (coclosedCompact X) ⊔ pure ∞
[PROOFSTEP]
rw [← nhdsWithin_compl_infty_eq, nhdsWithin_compl_singleton_sup_pure]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ HasBasis (𝓝 ∞) (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}
[PROOFSTEP]
rw [nhds_infty_eq]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ HasBasis (map some (coclosedCompact X) ⊔ pure ∞) (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}
[PROOFSTEP]
exact (hasBasis_coclosedCompact.map _).sup_pure _
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ comap some (𝓝 ∞) = coclosedCompact X
[PROOFSTEP]
simp [nhds_infty_eq, comap_sup, comap_map coe_injective]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
f : Filter (OnePoint X)
⊢ f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed s → IsCompact s → some '' sᶜ ∪ {∞} ∈ f
[PROOFSTEP]
simp only [hasBasis_nhds_infty.ge_iff, and_imp]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
f : Ultrafilter (OnePoint X)
⊢ ↑f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed s → IsCompact s → ¬some '' s ∈ f
[PROOFSTEP]
simp only [le_nhds_infty, ← compl_image_coe, Ultrafilter.mem_coe, Ultrafilter.compl_mem_iff_not_mem]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
α : Type u_2
f : OnePoint X → α
l : Filter α
⊢ Tendsto f (𝓝 ∞) l ↔ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l
[PROOFSTEP]
simp [nhds_infty_eq, and_comm]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
α : Type u_2
f : OnePoint X → α
l : Filter α
⊢ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l ↔
    ∀ (s : Set α), s ∈ l → f ∞ ∈ s ∧ ∃ t, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s
[PROOFSTEP]
simp only [tendsto_pure_left, hasBasis_coclosedCompact.tendsto_left_iff, forall_and, and_assoc, exists_prop]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
Y : Type u_2
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
⊢ Tendsto (f ∘ some) (coclosedCompact X) (𝓝 (f ∞)) ↔
    ∀ (s : Set Y), s ∈ 𝓝 (f ∞) → ∃ t, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s
[PROOFSTEP]
simp only [hasBasis_coclosedCompact.tendsto_left_iff, and_assoc]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
Y : Type u_2
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ ContinuousAt f ↑x ↔ ContinuousAt (f ∘ some) x
[PROOFSTEP]
rw [ContinuousAt, nhds_coe_eq, tendsto_map'_iff, ContinuousAt]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
Y : Type u_2
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto (f ∘ some) (𝓝 x) (𝓝 (f ↑x)) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : NoncompactSpace X
⊢ DenseRange some
[PROOFSTEP]
rw [DenseRange, ← compl_infty]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : NoncompactSpace X
⊢ Dense {∞}ᶜ
[PROOFSTEP]
exact dense_compl_singleton _
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x y : OnePoint X
⊢ Inseparable x y ↔ x = ∞ ∧ y = ∞ ∨ ∃ x', x = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
induction x using OnePoint.rec
[GOAL]
case h₁
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
y : OnePoint X
⊢ Inseparable ∞ y ↔ ∞ = ∞ ∧ y = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
induction y using OnePoint.rec
[GOAL]
case h₂
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
y : OnePoint X
x✝ : X
⊢ Inseparable (↑x✝) y ↔ ↑x✝ = ∞ ∧ y = ∞ ∨ ∃ x', ↑x✝ = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
induction y using OnePoint.rec
[GOAL]
case h₁.h₁
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ Inseparable ∞ ∞ ↔ ∞ = ∞ ∧ ∞ = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', ∞ = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]
[GOAL]
case h₁.h₂
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x✝ : X
⊢ Inseparable ∞ ↑x✝ ↔ ∞ = ∞ ∧ ↑x✝ = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', ↑x✝ = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]
[GOAL]
case h₂.h₁
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x✝ : X
⊢ Inseparable ↑x✝ ∞ ↔ ↑x✝ = ∞ ∧ ∞ = ∞ ∨ ∃ x', ↑x✝ = ↑x' ∧ ∃ y', ∞ = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]
[GOAL]
case h₂.h₂
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x✝¹ x✝ : X
⊢ Inseparable ↑x✝¹ ↑x✝ ↔ ↑x✝¹ = ∞ ∧ ↑x✝ = ∞ ∨ ∃ x', ↑x✝¹ = ↑x' ∧ ∃ y', ↑x✝ = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ IsCompact univ
[PROOFSTEP]
have : Tendsto ((↑) : X → OnePoint X) (cocompact X) (𝓝 ∞) :=
  by
  rw [nhds_infty_eq]
  exact (tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ Tendsto some (cocompact X) (𝓝 ∞)
[PROOFSTEP]
rw [nhds_infty_eq]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ Tendsto some (cocompact X) (map some (coclosedCompact X) ⊔ pure ∞)
[PROOFSTEP]
exact (tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact univ
[PROOFSTEP]
rw [← insert_none_range_some X]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact (insert none (range Option.some))
[PROOFSTEP]
exact this.isCompact_insert_range_of_cocompact continuous_coe
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T0Space X
⊢ T0Space (OnePoint X)
[PROOFSTEP]
refine' ⟨fun x y hxy => _⟩
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T0Space X
x y : OnePoint X
hxy : Inseparable x y
⊢ x = y
[PROOFSTEP]
rcases inseparable_iff.1 hxy with (⟨rfl, rfl⟩ | ⟨x, rfl, y, rfl, h⟩)
[GOAL]
case inl.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T0Space X
hxy : Inseparable ∞ ∞
⊢ ∞ = ∞
case inr.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T0Space X
x y : X
h : Inseparable x y
hxy : Inseparable ↑x ↑y
⊢ ↑x = ↑y
[PROOFSTEP]
exacts [rfl, congr_arg some h.eq]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T1Space X
z : OnePoint X
⊢ IsClosed {z}
[PROOFSTEP]
induction z using OnePoint.rec
[GOAL]
case h₁
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T1Space X
⊢ IsClosed {∞}
[PROOFSTEP]
exact isClosed_infty
[GOAL]
case h₂
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T1Space X
x✝ : X
⊢ IsClosed {↑x✝}
[PROOFSTEP]
rw [← image_singleton, isClosed_image_coe]
[GOAL]
case h₂
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T1Space X
x✝ : X
⊢ IsClosed {x✝} ∧ IsCompact {x✝}
[PROOFSTEP]
exact ⟨isClosed_singleton, isCompact_singleton⟩
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
⊢ NormalSpace (OnePoint X)
[PROOFSTEP]
have key : ∀ z : X, Disjoint (𝓝 (some z)) (𝓝 ∞) := fun z =>
  by
  rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact, disjoint_map coe_injective, ←
    principal_singleton, disjoint_principal_right, compl_infty]
  exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
z : X
⊢ Disjoint (𝓝 ↑z) (𝓝 ∞)
[PROOFSTEP]
rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact, disjoint_map coe_injective, ←
  principal_singleton, disjoint_principal_right, compl_infty]
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
z : X
⊢ Disjoint (𝓝 z) (cocompact X) ∧ range some ∈ map some (𝓝 z)
[PROOFSTEP]
exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
⊢ NormalSpace (OnePoint X)
[PROOFSTEP]
suffices : T2Space (OnePoint X)
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
this : T2Space (OnePoint X)
⊢ NormalSpace (OnePoint X)
case this
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
⊢ T2Space (OnePoint X)
[PROOFSTEP]
exact normalOfCompactT2
[GOAL]
case this
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
⊢ T2Space (OnePoint X)
[PROOFSTEP]
refine t2Space_iff_disjoint_nhds.2 fun x y hxy => ?_
[GOAL]
case this
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x y : OnePoint X
hxy : x ≠ y
⊢ Disjoint (𝓝 x) (𝓝 y)
[PROOFSTEP]
induction x using OnePoint.rec
[GOAL]
case this.h₁
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
y : OnePoint X
hxy : ∞ ≠ y
⊢ Disjoint (𝓝 ∞) (𝓝 y)
[PROOFSTEP]
induction y using OnePoint.rec
[GOAL]
case this.h₂
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
y : OnePoint X
x✝ : X
hxy : ↑x✝ ≠ y
⊢ Disjoint (𝓝 ↑x✝) (𝓝 y)
[PROOFSTEP]
induction y using OnePoint.rec
[GOAL]
case this.h₁.h₁
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
hxy : ∞ ≠ ∞
⊢ Disjoint (𝓝 ∞) (𝓝 ∞)
[PROOFSTEP]
exact (hxy rfl).elim
[GOAL]
case this.h₁.h₂
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
hxy : ∞ ≠ ↑x✝
⊢ Disjoint (𝓝 ∞) (𝓝 ↑x✝)
[PROOFSTEP]
exact (key _).symm
[GOAL]
case this.h₂.h₁
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
hxy : ↑x✝ ≠ ∞
⊢ Disjoint (𝓝 ↑x✝) (𝓝 ∞)
[PROOFSTEP]
exact key _
[GOAL]
case this.h₂.h₂
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
hxy : ↑x✝¹ ≠ ↑x✝
⊢ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)
[PROOFSTEP]
rwa [nhds_coe_eq, nhds_coe_eq, disjoint_map coe_injective, disjoint_nhds_nhds, ← coe_injective.ne_iff]
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
⊢ ¬Continuous ↑CofiniteTopology.of.symm
[PROOFSTEP]
inhabit X
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Continuous ↑CofiniteTopology.of.symm
[PROOFSTEP]
simp only [continuous_iff_continuousAt, ContinuousAt, not_forall]
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ∃ x, ¬Tendsto (↑CofiniteTopology.of.symm) (𝓝 x) (𝓝 (↑CofiniteTopology.of.symm x))
[PROOFSTEP]
use CofiniteTopology.of ↑(default : X)
[GOAL]
case h
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Tendsto (↑CofiniteTopology.of.symm) (𝓝 (↑CofiniteTopology.of ↑default))
      (𝓝 (↑CofiniteTopology.of.symm (↑CofiniteTopology.of ↑default)))
[PROOFSTEP]
simpa [nhds_coe_eq, nhds_discrete, CofiniteTopology.nhds_eq] using
  (finite_singleton ((default : X) : OnePoint X)).infinite_compl
