α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 a = pure a ⊔ f
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
⊢ 𝓝 a = pure a ⊔ f
letI := nhdsAdjoint a f
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ U ∈ 𝓝 a ↔ U ∈ pure a ⊔ f
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 a = pure a ⊔ f
ext U
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) ↔ U ∈ pure a ⊔ f
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ U ∈ 𝓝 a ↔ U ∈ pure a ⊔ f
rw [mem_nhds_iff]
case a.mp
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) → U ∈ pure a ⊔ f

case a.mpr
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ U ∈ pure a ⊔ f → ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) ↔ U ∈ pure a ⊔ f
constructor
case a.mp.intro.intro.intro
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U t : Set α
htU : t ⊆ U
ht : IsOpen t
hat : a ∈ t
⊢ U ∈ pure a ⊔ f
case a.mp
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ (∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t) → U ∈ pure a ⊔ f
rintro ⟨t, htU, ht, hat⟩
no goals
case a.mp.intro.intro.intro
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U t : Set α
htU : t ⊆ U
ht : IsOpen t
hat : a ∈ t
⊢ U ∈ pure a ⊔ f
exact ⟨htU hat, mem_of_superset (ht hat) htU⟩
case a.mpr.intro
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
haU : U ∈ (pure a).sets
hU : U ∈ f.sets
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
case a.mpr
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
⊢ U ∈ pure a ⊔ f → ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
rintro ⟨haU, hU⟩
no goals
case a.mpr.intro
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
haU : U ∈ (pure a).sets
hU : U ∈ f.sets
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ a ∈ t
exact ⟨U, Subset.rfl, fun _ => hU, haU⟩