[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α✝
x : α✝
α : Type u_3
inst✝ : TopologicalSpace (α × α)
⊢ 𝓝ˢ (diagonal α) = ⨆ (x : α), 𝓝 (x, x)
[PROOFSTEP]
rw [nhdsSet, ← range_diag, ← range_comp]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α✝
x : α✝
α : Type u_3
inst✝ : TopologicalSpace (α × α)
⊢ sSup (range (𝓝 ∘ fun x => (x, x))) = ⨆ (x : α), 𝓝 (x, x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ s ∈ 𝓝ˢ t ↔ ∀ (x : α), x ∈ t → s ∈ 𝓝 x
[PROOFSTEP]
simp_rw [nhdsSet, Filter.mem_sSup, ball_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ s ⊆ interior t ↔ t ∈ 𝓝ˢ s
[PROOFSTEP]
simp_rw [mem_nhdsSet_iff_forall, subset_interior_iff_nhds]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure s) t
[PROOFSTEP]
rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl, subset_compl_iff_disjoint_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure t)
[PROOFSTEP]
rw [disjoint_comm, disjoint_principal_nhdsSet, disjoint_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ s ∈ 𝓝ˢ t ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s
[PROOFSTEP]
rw [← subset_interior_iff_mem_nhdsSet, subset_interior_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s₁ s₂ t₁ t₂ : Set α
x : α
s t : Set α
⊢ t ∈ 𝓝ˢ s ↔ ∃ i, (IsOpen i ∧ s ⊆ i) ∧ i ⊆ t
[PROOFSTEP]
simp [mem_nhdsSet_iff_exists, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
hU : IsOpen s
⊢ s ∈ 𝓝ˢ t ↔ t ⊆ s
[PROOFSTEP]
rw [← subset_interior_iff_mem_nhdsSet, hU.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ 𝓝ˢ s = 𝓟 s ↔ IsOpen s
[PROOFSTEP]
rw [← principal_le_nhdsSet.le_iff_eq, le_principal_iff, mem_nhdsSet_iff_forall, isOpen_iff_mem_nhds]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ 𝓝ˢ {x} = 𝓝 x
[PROOFSTEP]
simp [nhdsSet]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ 𝓝ˢ ∅ = ⊥
[PROOFSTEP]
rw [isOpen_empty.nhdsSet_eq, principal_empty]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ s ∈ 𝓝ˢ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ 𝓝ˢ univ = ⊤
[PROOFSTEP]
rw [isOpen_univ.nhdsSet_eq, principal_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s₁ s₂ t₁ t₂ : Set α
x : α
s t : Set α
⊢ 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t
[PROOFSTEP]
simp only [nhdsSet, image_union, sSup_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)
[PROOFSTEP]
rw [nhdsSet_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂
[PROOFSTEP]
exact union_mem_sup h₁ h₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s₁ s₂ t₁ t₂ : Set α
x✝ x : α
s : Set α
⊢ 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s
[PROOFSTEP]
rw [insert_eq, nhdsSet_union, nhdsSet_singleton]
