fixedPoints_of_subsingleton — Mathlib

English

If α is a Subsingleton, then every element is fixed by G; hence fixedPoints G α = univ.

Русский

Если α — подмножество, то все элементы зафиксированы G; следовательно, fixedPoints G α = univ.

LaTeX

$$fixedPoints G α = univ$$

Lean4

@[to_additive]
theorem fixedPoints_of_subsingleton [Subsingleton α] : fixedPoints G α = .univ :=
  by
  apply Set.eq_univ_of_forall
  simp only [mem_fixedPoints]
  intro x hx
  apply Subsingleton.elim ..

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