no goals
G : Type u_2
H : Type ?u.463396
α : Type u_1
β : Type ?u.463402
E : Type ?u.463405
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
⊢ x ∈ fundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 1 ∧ x ∈ g • s
simp [fundamentalFrontier]