α : Type u
β : Type v
ι : Sort w
a : α
s s₁✝ s₂✝ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
x : α
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
α : Type u
β : Type v
ι : Sort w
a : α
s s₁✝ s₂✝ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
x : α
h : x ∈ closure (s₁ ∪ s₂)
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ x ∈ closure s₂
rw [mem_closure_iff_nhds_neBot] at *
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁✝ s₂✝ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
x : α
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
rwa [←
  calc
    𝓝 x ⊓ principal (s₁ ∪ s₂) = 𝓝 x ⊓ (principal s₁ ⊔ principal s₂) := by rw [sup_principal]
    _ = 𝓝 x ⊓ principal s₁ ⊔ 𝓝 x ⊓ principal s₂ := inf_sup_left
    _ = ⊥ ⊔ 𝓝 x ⊓ principal s₂ := by rw [inf_principal_eq_bot.mpr h₁]
    _ = 𝓝 x ⊓ principal s₂ := bot_sup_eq
    ]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁✝ s₂✝ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
x : α
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) = 𝓝 x ⊓ (𝓟 s₁ ⊔ 𝓟 s₂)
rw [sup_principal]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁✝ s₂✝ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
x : α
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₁ ⊔ 𝓝 x ⊓ 𝓟 s₂ = ⊥ ⊔ 𝓝 x ⊓ 𝓟 s₂
rw [inf_principal_eq_bot.mpr h₁]