finite_compl_fixedBy_swap — Mathlib

English

The complement of the fixed-by set of the swap x y is finite.

Русский

Дополнение множества фиксирования для транспозиции x↔y конечно.

LaTeX

$$(fixedBy α (swap x y))^{c}.Finite$$

Lean4

theorem finite_compl_fixedBy_swap {x y : α} : (fixedBy α (swap x y))ᶜ.Finite :=
  Set.Finite.subset (s := { x, y }) (by simp)
    (compl_subset_comm.mp fun z h ↦ by apply swap_apply_of_ne_of_ne <;> rintro rfl <;> simp at h)

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