fst

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#ONote.NF.fst

English

If b1 ≤ b2 and NFBelow o b1 then NFBelow o b2.

Русский

Если b1 ≤ b2 и NFBelow o b1, то NFBelow o b2.

LaTeX

$$$(b_1 \le b_2) \Rightarrow (NFBelow(o,b_1) \Rightarrow NFBelow(o,b_2))$$$

Lean4

theorem fst {e n a} : NF (oadd e n a) → NF e
  | ⟨⟨_, h⟩⟩ => h.fst

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

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

Разделы

Аффилиация

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