mem_fixedPoints' — Mathlib

English

There exists an equivalence between a ∈ fixedPoints M α and ∀ a' with a' in orbit M a, a' = a.

Русский

Существует эквивалентность: a ∈ fixedPoints M α тогда и только тогда, когда для всех a' ∈ орбиты a, a' = a.

LaTeX

$$$$ a \\in \\mathrm{fixedPoints}(M, \\alpha) \\iff \\forall a' (a' \\in \\mathrm{orbit}(M, a) \\rightarrow a' = a). $$$$

Lean4

@[to_additive]
theorem mem_fixedPoints' {a : α} : a ∈ fixedPoints M α ↔ ∀ a', a' ∈ orbit M a → a' = a :=
  ⟨fun h _ h₁ =>
    let ⟨m, hm⟩ := mem_orbit_iff.1 h₁
    hm ▸ h m,
    fun h _ => h _ (mem_orbit _ _)⟩

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