add_nfBelow — Mathlib

English

If o1 below b and o2 below b in NF sense, then o1 + o2 is below b with NF property preserved.

Русский

Если o1 и o2 соответствуют нижнему пределу NF относительно b, то сумма o1 + o2 сохраняет NF-близость к b.

LaTeX

$$$\forall b : ONote, \forall o_1 o_2 : ONote,\; o_1.NFBelow\; b \rightarrow o_2.NFBelow\; b \rightarrow (o_1 + o_2).NFBelow\; b$$$

Lean4

theorem add_nfBelow {b} : ∀ {o₁ o₂}, NFBelow o₁ b → NFBelow o₂ b → NFBelow (o₁ + o₂) b
  | 0, _, _, h₂ => h₂
  | oadd e n a, o, h₁, h₂ => by
    have h' := add_nfBelow (h₁.snd.mono <| le_of_lt h₁.lt) h₂
    simp only [oadd_add]; revert h'; obtain - | ⟨e', n', a'⟩ := a + o <;> intro h'
    · exact NFBelow.oadd h₁.fst NFBelow.zero h₁.lt
    have : ((e.cmp e').Compares e e') := @cmp_compares _ _ h₁.fst h'.fst
    cases h : cmp e e' <;> dsimp [addAux] <;> simp only [h]
    · exact h'
    · simp only [h] at this
      subst e'
      exact NFBelow.oadd h'.fst h'.snd h'.lt
    · simp only [h] at this
      exact NFBelow.oadd h₁.fst (NF.below_of_lt this ⟨⟨_, h'⟩⟩) h₁.lt

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