two_le_card_support

Mathlib.GroupTheory.Perm.Cycle.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.IsCycle.two_le_card_support

English

For an IsCycle f, the support of f has size at least 2. More precisely, |f.support| ≥ 2.

Русский

Для IsCycle f опора f имеет размер по крайней мере 2. Точнее, |f.support| ≥ 2.

LaTeX

$$IsCycle.two_le_card_support$$

Lean4

theorem two_le_card_support (h : IsCycle f) : 2 ≤ #f.support :=
  two_le_card_support_of_ne_one h.ne_one

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru