principal_add_one

Mathlib.SetTheory.Ordinal.Principal

URI: https://scilib.ai/kg/mathlib#Ordinal.principal_add_one

English

1 is an additive principal: for every a with a < 1, we have a + 1 = 1.

Русский

1 является принципиальным для сложения: для каждого a, если a < 1, то a + 1 = 1.

LaTeX

$$$\forall a\,(a < 1 \rightarrow a + 1 = 1).$$$

Lean4

theorem principal_add_one : Principal (· + ·) 1 :=
  principal_one_iff.2 <| zero_add 0

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

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

Разделы

Аффилиация

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