length_toList_pos_of_mem_support

Mathlib.GroupTheory.Perm.Cycle.Concrete

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

← MathLib Explorer

English

If x lies in the support of p, then length of toList p x is positive.

Русский

Если x принадлежит поддержке p, то длина toList p x положительная.

LaTeX

$$$$x \in p.\mathrm{support} \Rightarrow 0 < \mathrm{length}(\mathrm{toList}\ p\ x).$$$$

Lean4

theorem length_toList_pos_of_mem_support (h : x ∈ p.support) : 0 < length (toList p x) :=
  zero_lt_two.trans_le (two_le_length_toList_iff_mem_support.mpr h)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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