isChain_two_cons_primeFactorsList

Mathlib.Data.Nat.Factors

URI: https://scilib.ai/kg/mathlib#Nat.isChain_two_cons_primeFactorsList

← MathLib Explorer

English

The list starting with 2 followed by the primeFactorsList(n) is a chain under ≤.

Русский

Список, начинающийся с 2 и продолженный primeFactorsList(n), упорядочен по ≤.

LaTeX

$$$ \text{List.IsChain}( (\le) ) (2 :: \text{primeFactorsList}(n)) $$$

Lean4

theorem isChain_two_cons_primeFactorsList (n) : List.IsChain (· ≤ ·) (2 :: primeFactorsList n) :=
  isChain_cons_primeFactorsList fun _ pp _ => pp.two_le

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

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

Разделы

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

Аффилиация

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