fundamentalSequenceProp_inl_none

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#ONote.fundamentalSequenceProp_inl_none

English

FundamentalSequenceProp applied to Sum.inl none is equivalent to o being zero.

Русский

FundamentalSequenceProp, применённое к Sum.inl none, эквивалентно тому, что o = 0.

LaTeX

$$$\\text{FundamentalSequenceProp}(o)(\\text{Sum.inl none}) \\iff o = 0$$$

Lean4

theorem fundamentalSequenceProp_inl_none (o) : FundamentalSequenceProp o (Sum.inl none) ↔ o = 0 :=
  Iff.rfl

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

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

Разделы

Аффилиация

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