α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
⊢ 𝓝ˢ s ≤ 𝓝ˢ t → s ⊆ t
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t
refine' ⟨_, fun h => monotone_nhdsSet h⟩
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
⊢ (∀ (x : Set α), x ∈ 𝓝ˢ t → x ∈ 𝓝ˢ s) → s ⊆ t
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
⊢ 𝓝ˢ s ≤ 𝓝ˢ t → s ⊆ t
simp_rw [Filter.le_def]
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
h : ∀ (x : Set α), x ∈ 𝓝ˢ t → x ∈ 𝓝ˢ s
x : α
hx : x ∈ s
⊢ x ∈ t
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
⊢ (∀ (x : Set α), x ∈ 𝓝ˢ t → x ∈ 𝓝ˢ s) → s ⊆ t
intro h x hx
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
x : α
hx : x ∈ s
h : {x}ᶜ ∈ 𝓝ˢ t → {x}ᶜ ∈ 𝓝ˢ s
⊢ x ∈ t
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
h : ∀ (x : Set α), x ∈ 𝓝ˢ t → x ∈ 𝓝ˢ s
x : α
hx : x ∈ s
⊢ x ∈ t
specialize h ({x}ᶜ)
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
x : α
hx : x ∈ s
h : ¬x ∈ t → ¬x ∈ s
⊢ x ∈ t
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
x : α
hx : x ∈ s
h : {x}ᶜ ∈ 𝓝ˢ t → {x}ᶜ ∈ 𝓝ˢ s
⊢ x ∈ t
simp_rw [compl_singleton_mem_nhdsSet_iff] at h
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
x : α
hx : x ∈ s
h : ¬x ∈ t → ¬x ∈ s
hxt : ¬x ∈ t
⊢ False
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
x : α
hx : x ∈ s
h : ¬x ∈ t → ¬x ∈ s
⊢ x ∈ t
by_contra hxt
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
x : α
hx : x ∈ s
h : ¬x ∈ t → ¬x ∈ s
hxt : ¬x ∈ t
⊢ False
exact h hxt hx