add_nf — Mathlib

English

If o1 and o2 are NF, then o1 + o2 is NF.

Русский

Если оба слагаемых NF, то сумма NF.

LaTeX

$$$\forall o_1,o_2,\; [o_1.NF] \rightarrow [o_2.NF] \rightarrow NF (o_1 + o_2)$$$

Lean4

instance add_nf (o₁ o₂) : ∀ [NF o₁] [NF o₂], NF (o₁ + o₂)
  | ⟨⟨b₁, h₁⟩⟩, ⟨⟨b₂, h₂⟩⟩ =>
    ⟨(le_total b₁ b₂).elim (fun h => ⟨b₂, add_nfBelow (h₁.mono h) h₂⟩) fun h => ⟨b₁, add_nfBelow h₁ (h₂.mono h)⟩⟩

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