mul_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

protected theorem mul_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
    ⟨_, mul_pos F0 G0, i, fun _ ij =>
      let ⟨h₁, h₂⟩ := h _ ij
      mul_le_mul h₁ h₂ (le_of_lt G0) (le_trans (le_of_lt F0) h₁)⟩

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