of_le — Mathlib

English

If a is strictly positive and a ≤ b, then b is strictly positive.

Русский

Если a строго положительно, и a ≤ b, то b строго положительно.

LaTeX

$$ha : IsStrictlyPositive a, hab : a ≤ b \\Rightarrow IsStrictlyPositive b$$

Lean4

protected theorem _root_.IsStrictlyPositive.of_le {a b : A} (ha : IsStrictlyPositive a) (hab : a ≤ b) :
    IsStrictlyPositive b :=
  ⟨ha.nonneg.trans hab, CStarAlgebra.isUnit_of_le ha.isUnit ha.nonneg hab⟩

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