fixed_eq_iInter_fixedBy — Mathlib

English

Let M act on α. Then fixedPoints(M, α) equals the intersection over all m ∈ M of fixedBy(m).

Русский

Пусть M действует на α. Тогда фиксированные точки равны пересечению по всем m ∈ M фиксирований m.

LaTeX

$$$$\\mathrm{fixedPoints}(M, \\alpha) = \\bigcap_{m \\in M} \\mathrm{fixedBy}(m). $$$$

Lean4

@[to_additive]
theorem fixed_eq_iInter_fixedBy : fixedPoints M α = ⋂ m : M, fixedBy α m :=
  Set.ext fun _ => ⟨fun hx => Set.mem_iInter.2 fun m => hx m, fun hx m => (Set.mem_iInter.1 hx m :)⟩

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