X : Type u_1
Y : Type ?u.17180
Z : Type ?u.17183
α : Type ?u.17186
ι : Type ?u.17189
π : ι → Type ?u.17194
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (¬∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ ¬y ∈ S
X : Type u_1
Y : Type ?u.17180
Z : Type ?u.17183
α : Type ?u.17186
ι : Type ?u.17189
π : ι → Type ?u.17194
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ ¬x ⤳ y ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ ¬y ∈ S
rw [specializes_iff_forall_closed]
X : Type u_1
Y : Type ?u.17180
Z : Type ?u.17183
α : Type ?u.17186
ι : Type ?u.17189
π : ι → Type ?u.17194
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (∃ s, IsClosed s ∧ x ∈ s ∧ ¬y ∈ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ ¬y ∈ S
X : Type u_1
Y : Type ?u.17180
Z : Type ?u.17183
α : Type ?u.17186
ι : Type ?u.17189
π : ι → Type ?u.17194
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (¬∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ ¬y ∈ S
push_neg
no goals
X : Type u_1
Y : Type ?u.17180
Z : Type ?u.17183
α : Type ?u.17186
ι : Type ?u.17189
π : ι → Type ?u.17194
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (∃ s, IsClosed s ∧ x ∈ s ∧ ¬y ∈ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ ¬y ∈ S
rfl