oadd_lt_oadd_1 — Mathlib

English

If h1: NF(oadd e1 n1 o1) and h: e1 < e2, then oadd e1 n1 o1 < oadd e2 n2 o2.

Русский

Если h1: NF(oadd(e1,n1,o1)) и e1 < e2, то oadd(e1,n1,o1) < oadd(e2,n2,o2).

LaTeX

$$$NF(\mathrm{oadd}(e_1,n_1,o_1)) \land e_1 < e_2 \Rightarrow \mathrm{oadd}(e_1,n_1,o_1) < \mathrm{oadd}(e_2,n_2,o_2)$$$

Lean4

theorem oadd_lt_oadd_1 {e₁ n₁ o₁ e₂ n₂ o₂} (h₁ : NF (oadd e₁ n₁ o₁)) (h : e₁ < e₂) : oadd e₁ n₁ o₁ < oadd e₂ n₂ o₂ :=
  @lt_of_lt_of_le _ _ (repr (oadd e₁ n₁ o₁)) _ _ (NF.below_of_lt h h₁).repr_lt (omega0_le_oadd e₂ n₂ o₂)

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