English
A subset s of α is fixed by g if and only if g leaves s invariant elementwise, i.e., s ∈ fixedBy (Set α) g iff ∀ x ∈ α, g • x ∈ s ⇔ x ∈ s.
Русский
Подмножество s множества α фиксируется относительно g тогда и только тогда, когда g отображает s в себя покомпонентно: s ∈ fixedBy (Set α) g ↔ ∀ x, g • x ∈ s ⇔ x ∈ s.
LaTeX
$$$ s \in fixedBy(Set\ α, g) \iff \forall x, g \cdot x \in s \iff x \in s $$$
Lean4
/-- If a set `s : Set α` is in `fixedBy (Set α) g`, then all points of `s` will stay in `s` after being
moved by `g`.
-/
@[to_additive /-- If a set `s : Set α` is in `fixedBy (Set α) g`, then all points of `s` will stay
in `s` after being moved by `g`. -/
]
theorem set_mem_fixedBy_iff (s : Set α) (g : G) : s ∈ fixedBy (Set α) g ↔ ∀ x, g • x ∈ s ↔ x ∈ s := by
simp_rw [mem_fixedBy, ← eq_inv_smul_iff, Set.ext_iff, Set.mem_inv_smul_set_iff, Iff.comm]
