hasProd_strict_mono — Mathlib

English

If HasProd f a1 and HasProd g a2 and f < g in the product order, then a1 < a2.

Русский

Если HasProd f a1 и HasProd g a2 и f < g по порядку произведений, то a1 < a2.

LaTeX

$$$\\forall f,g:\\, \\text{HasProd } f a_1 \\to \\text{HasProd } g a_2 \\to \\text{Pi.preorder.lt } f g \\to a_1 < a_2$$$

Lean4

@[to_additive (attr := mono)]
theorem hasProd_strict_mono (hf : HasProd f a₁) (hg : HasProd g a₂) (h : f < g) : a₁ < a₂ :=
  let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
  hasProd_lt hle hi hf hg

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