nf_scale

Mathlib.SetTheory.Ordinal.Notation

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

English

If x and o are NF, then scale x o is NF.

Русский

Если x и o являются NF, то scale x o также NF.

LaTeX

$$$\\text{NF}(x) \\Rightarrow \\text{NF}(o) \\Rightarrow \\text{NF}(\\mathrm{scale}\\ x\\ o)$$$

Lean4

instance nf_scale (x) [NF x] (o) [NF o] : NF (scale x o) :=
  by
  rw [scale_eq_mul]
  infer_instance

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

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

Разделы

Аффилиация

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