add_pos — Mathlib

English

If f and g are positive, then f+g is positive.

Русский

Если f и g положительны, то f+g положителен.

LaTeX

$$$ \text{Pos}(f) \land \text{Pos}(g) \Rightarrow \text{Pos}(f+g) $$$

Lean4

theorem add_pos {f g : CauSeq α abs} : Pos f → Pos g → Pos (f + g)
  | ⟨_, F0, hF⟩, ⟨_, G0, hG⟩ =>
    let ⟨i, h⟩ := exists_forall_ge_and hF hG
    ⟨_, _root_.add_pos F0 G0, i, fun _ ij =>
      let ⟨h₁, h₂⟩ := h _ ij
      add_le_add h₁ h₂⟩

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