X : Type u_1
Y : Type ?u.16860
Z : Type ?u.16863
α : Type ?u.16866
ι : Type ?u.16869
π : ι → Type ?u.16874
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), IsOpen s → y ∈ s → x ∈ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ ¬x ∈ S
X : Type u_1
Y : Type ?u.16860
Z : Type ?u.16863
α : Type ?u.16866
ι : Type ?u.16869
π : ι → Type ?u.16874
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, IsOpen S ∧ y ∈ S ∧ ¬x ∈ S
rw [specializes_iff_forall_open]
X : Type u_1
Y : Type ?u.16860
Z : Type ?u.16863
α : Type ?u.16866
ι : Type ?u.16869
π : ι → Type ?u.16874
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (∃ s, IsOpen s ∧ y ∈ s ∧ ¬x ∈ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ ¬x ∈ S
X : Type u_1
Y : Type ?u.16860
Z : Type ?u.16863
α : Type ?u.16866
ι : Type ?u.16869
π : ι → Type ?u.16874
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), IsOpen s → y ∈ s → x ∈ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ ¬x ∈ S
push_neg
no goals
X : Type u_1
Y : Type ?u.16860
Z : Type ?u.16863
α : Type ?u.16866
ι : Type ?u.16869
π : ι → Type ?u.16874
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (∃ s, IsOpen s ∧ y ∈ s ∧ ¬x ∈ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ ¬x ∈ S
rfl