α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ closure (s ∩ t) ∩ (closure (sᶜ) ∪ closure (tᶜ)) ⊆
    closure s ∩ closure (sᶜ) ∩ closure t ∪ closure s ∩ (closure t ∩ closure (tᶜ))
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t
simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ closure s ∩ closure t ∩ (closure (sᶜ) ∪ closure (tᶜ)) =
    closure s ∩ closure (sᶜ) ∩ closure t ∪ closure s ∩ (closure t ∩ closure (tᶜ))
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ closure (s ∩ t) ∩ (closure (sᶜ) ∪ closure (tᶜ)) ⊆
    closure s ∩ closure (sᶜ) ∩ closure t ∪ closure s ∩ (closure t ∩ closure (tᶜ))
refine' (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq _
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ closure s ∩ closure t ∩ (closure (sᶜ) ∪ closure (tᶜ)) =
    closure s ∩ closure (sᶜ) ∩ closure t ∪ closure s ∩ (closure t ∩ closure (tᶜ))
simp only [inter_distrib_left, inter_distrib_right, inter_assoc, inter_comm (closure t)]