below_of_lt — Mathlib

English

If repr e < b, then NF(oadd e n a) → NFBelow (oadd e n a) b.

Русский

Если repr e < b, то NF(oadd e n a) означает NFBelow (oadd e n a) b.

LaTeX

$$$(\operatorname{repr}(e) < b) \Rightarrow NF(\mathrm{oadd}(e,n,a)) \Rightarrow NFBelow(\mathrm{oadd}(e,n,a), b)$$$

Lean4

theorem below_of_lt {e n a b} (H : repr e < b) : NF (ONote.oadd e n a) → NFBelow (ONote.oadd e n a) b
  | ⟨⟨b', h⟩⟩ => by (obtain - | ⟨h₁, h₂, h₃⟩ := h; exact NFBelow.oadd' h₁ h₂ H)

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