no goals
α : Type u
β : Type v
ι : Type ?u.71012
π : ι → Type ?u.71017
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : PreconnectedSpace α
s : Set α
⊢ Set.Nonempty (frontier s) ↔ Set.Nonempty s ∧ s ≠ univ
simp only [nonempty_iff_ne_empty, Ne.def, frontier_eq_empty_iff, not_or]