support_finRotate_of_le — Mathlib

English

If 2 ≤ n, then the support of finRotate(n) is the full set univ.

Русский

Если 2 ≤ n, то опора finRotate(n) равна полной множеству.

LaTeX

$$$ \\operatorname{supp}(\\mathrm{finRotate}(n)) = \\operatorname{Finset.univ} \\quad \\text{при } 2 \\le n$$$

Lean4

theorem support_finRotate_of_le {n : ℕ} (h : 2 ≤ n) : support (finRotate n) = Finset.univ :=
  by
  obtain ⟨m, rfl⟩ := exists_add_of_le h
  rw [add_comm, support_finRotate]

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