α : Type u
β : Type v
ι : Type ?u.171474
π : ι → Type ?u.171479
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
⊢ interior s = s ∧ closure s = s ↔ closure s ⊆ interior s
α : Type u
β : Type v
ι : Type ?u.171474
π : ι → Type ?u.171479
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
⊢ IsClopen s ↔ frontier s = ∅
rw [IsClopen, ← closure_eq_iff_isClosed, ← interior_eq_iff_isOpen, frontier, diff_eq_empty]
α : Type u
β : Type v
ι : Type ?u.171474
π : ι → Type ?u.171479
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : closure s ⊆ interior s
⊢ interior s = s ∧ closure s = s
α : Type u
β : Type v
ι : Type ?u.171474
π : ι → Type ?u.171479
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
⊢ interior s = s ∧ closure s = s ↔ closure s ⊆ interior s
refine' ⟨fun h => (h.2.trans h.1.symm).subset, fun h => _⟩
no goals
α : Type u
β : Type v
ι : Type ?u.171474
π : ι → Type ?u.171479
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
h : closure s ⊆ interior s
⊢ interior s = s ∧ closure s = s
exact ⟨interior_subset.antisymm (subset_closure.trans h),
  (h.trans interior_subset).antisymm subset_closure⟩