α : Type u_1
β : Type ?u.398706
γ : Type ?u.398709
δ : Type ?u.398712
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ frontier (tᶜ) = s ∩ frontier (tᶜ)
α : Type u_1
β : Type ?u.398706
γ : Type ?u.398709
δ : Type ?u.398712
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ Set.ite t s s' ∩ closure (tᶜ) = s' ∩ closure (tᶜ)
rw [← ite_compl, ite_inter_closure_eq_of_inter_frontier_eq]
no goals
α : Type u_1
β : Type ?u.398706
γ : Type ?u.398709
δ : Type ?u.398712
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ frontier (tᶜ) = s ∩ frontier (tᶜ)
rwa [frontier_compl, eq_comm]