subsingleton_orbit_iff_mem_fixedPoints

English

The orbit of a is a singleton if and only if a is fixed by every element of M.

Русский

Орбита элемента является единичной тогда и только тогда, когда элемент фиксирован всем M.

LaTeX

$$(orbit M a).Subsingleton \iff a \in fixedPoints M α$$

Lean4

@[to_additive (attr := simp)]
theorem subsingleton_orbit_iff_mem_fixedPoints {a : α} : (orbit M a).Subsingleton ↔ a ∈ fixedPoints M α :=
  by
  rw [mem_fixedPoints]
  constructor
  · exact fun h m ↦ h (mem_orbit a m) (mem_orbit_self a)
  · rintro h _ ⟨m, rfl⟩ y ⟨p, rfl⟩
    simp only [h]

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