mem_fixedPoints_iff_card_orbit_eq_one

English

For a ∈ α, if the orbit is finite, then a is fixed by M if and only if the orbit has exactly one element.

Русский

Пусть для элемента a орбита конечна тогда и только тогда, когда a фиксирован на всём M, если и только если орбита состоит из одного элемента.

LaTeX

$$a in fixedPoints M α \iff card(orbit M a) = 1$$

Lean4

@[to_additive mem_fixedPoints_iff_card_orbit_eq_one]
theorem mem_fixedPoints_iff_card_orbit_eq_one {a : α} [Fintype (orbit M a)] :
    a ∈ fixedPoints M α ↔ Fintype.card (orbit M a) = 1 := by
  simp only [← subsingleton_orbit_iff_mem_fixedPoints, le_antisymm_iff, Fintype.card_le_one_iff_subsingleton,
    Nat.add_one_le_iff, Fintype.card_pos_iff, Set.subsingleton_coe, iff_self_and, Set.nonempty_coe_sort, nonempty_orbit,
    implies_true]

Похожие утверждения