to_covariantClass_pos_mul_le — Mathlib

English

If α is PosMulMono, then left-multiplication by any fixed element is monotone with respect to ≤.

Русский

Если α обладает свойством PosMulMono, то левое умножение на фиксированный элемент сохраняет порядок: x ≤ y ⇒ x·z ≤ y·z для любого z.

LaTeX

$$$\forall x,y,z \in \alpha,\ x \le y \Rightarrow x\cdot z \le y\cdot z$$$

Lean4

instance to_covariantClass_pos_mul_le [MulPosMono α] : CovariantClass α>0 α (fun x y => y * x) (· ≤ ·) :=
  ⟨fun a _ _ bc => @CovariantClass.elim α≥0 α (fun x y => y * x) (· ≤ ·) _ ⟨_, a.2.le⟩ _ _ bc⟩

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