α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
rw [le_iff_nhds]
case mp
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ (∀ (x : α), 𝓝 x ≤ 𝓝 x) → 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b

case mpr
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ (𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b) → ∀ (x : α), 𝓝 x ≤ 𝓝 x
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
constructor
case mp
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
case mp
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ (∀ (x : α), 𝓝 x ≤ 𝓝 x) → 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
intro h
case mp.left
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ 𝓝 a ≤ pure a ⊔ f

case mp.right
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ ∀ (b : α), b ≠ a → 𝓝 b = pure b
case mp
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
constructor
case mp.left
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ 𝓝 a
⊢ 𝓝 a ≤ pure a ⊔ f
case mp.left
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ 𝓝 a ≤ pure a ⊔ f
specialize h a
no goals
case mp.left
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ 𝓝 a
⊢ 𝓝 a ≤ pure a ⊔ f
rwa [nhdsAdjoint_nhds] at h
case mp.right
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
b : α
hb : b ≠ a
⊢ 𝓝 b = pure b
case mp.right
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ ∀ (b : α), b ≠ a → 𝓝 b = pure b
intro b hb
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
b : α
hb : b ≠ a
⊢ 𝓝 b ≤ pure b
case mp.right
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
b : α
hb : b ≠ a
⊢ 𝓝 b = pure b
apply le_antisymm _ (pure_le_nhds b)
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
b : α
hb : b ≠ a
h : 𝓝 b ≤ 𝓝 b
⊢ 𝓝 b ≤ pure b
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
b : α
hb : b ≠ a
⊢ 𝓝 b ≤ pure b
specialize h b
no goals
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
b : α
hb : b ≠ a
h : 𝓝 b ≤ 𝓝 b
⊢ 𝓝 b ≤ pure b
rwa [nhdsAdjoint_nhds_of_ne a f hb] at h
case mpr.intro
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ pure a ⊔ f
h' : ∀ (b : α), b ≠ a → 𝓝 b = pure b
b : α
⊢ 𝓝 b ≤ 𝓝 b
case mpr
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ (𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b) → ∀ (x : α), 𝓝 x ≤ 𝓝 x
rintro ⟨h, h'⟩ b
case pos
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ pure a ⊔ f
h' : ∀ (b : α), b ≠ a → 𝓝 b = pure b
b : α
hb : b = a
⊢ 𝓝 b ≤ 𝓝 b

case neg
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ pure a ⊔ f
h' : ∀ (b : α), b ≠ a → 𝓝 b = pure b
b : α
hb : ¬b = a
⊢ 𝓝 b ≤ 𝓝 b
case mpr.intro
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ pure a ⊔ f
h' : ∀ (b : α), b ≠ a → 𝓝 b = pure b
b : α
⊢ 𝓝 b ≤ 𝓝 b
by_cases hb : b = a
no goals
case pos
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ pure a ⊔ f
h' : ∀ (b : α), b ≠ a → 𝓝 b = pure b
b : α
hb : b = a
⊢ 𝓝 b ≤ 𝓝 b
rwa [hb, nhdsAdjoint_nhds]
no goals
case neg
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
h : 𝓝 a ≤ pure a ⊔ f
h' : ∀ (b : α), b ≠ a → 𝓝 b = pure b
b : α
hb : ¬b = a
⊢ 𝓝 b ≤ 𝓝 b
simp [nhdsAdjoint_nhds_of_ne a f hb, h' b hb]