sub_nf

Mathlib.SetTheory.Ordinal.Notation

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

English

There is a NF instance for subtraction: o1 - o2 is NF whenever o1 and o2 are ONote with NF.

Русский

Существование NF для вычитания: o1 - o2 NF при NF o1 и o2.

LaTeX

$$$\forall o_1,o_2 : ONote, [o_1.NF] [o_2.NF] \Rightarrow NF ((instHSub.hSub) o_1 o_2)$$$

Lean4

instance sub_nf (o₁ o₂) : ∀ [NF o₁] [NF o₂], NF (o₁ - o₂)
  | ⟨⟨b₁, h₁⟩⟩, h₂ => ⟨⟨b₁, sub_nfBelow h₁ h₂⟩⟩

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

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

Разделы

Аффилиация

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