α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen (u ∩ v)

α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen v

α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen u
α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ Set.Nonempty (closure s ∩ u) → Set.Nonempty (closure s ∩ v) → Set.Nonempty (closure s ∩ (u ∩ v)) ↔
    Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
iterate 3 rw [closure_inter_open_nonempty_iff]
no goals
α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen (u ∩ v)

α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen v

α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen u
exacts [hu.inter hv, hv, hu]
α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen (u ∩ v)

α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen v

α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen u
α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (closure s ∩ (u ∩ v)) ↔
    Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))

α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen v

α : Type u
β : Type v
ι : Type ?u.181256
π : ι → Type ?u.181261
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s u v : Set α
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen u
rw [closure_inter_open_nonempty_iff]