mulPosMono_iff_covariant_pos — Mathlib

English

MulPosMono α is equivalent to CovariantClass α>0 α (fun x y => y * x) (≤).

Русский

MulPosMono α эквивалентно CovariantClass α>0 α (функция умножения справа) (≤).

LaTeX

$$$$ MulPosMono \alpha \Longleftrightarrow CovariantClass \alpha>0 α (fun x y => y \cdot x) (\le). $$$$

Lean4

theorem mulPosMono_iff_covariant_pos : MulPosMono α ↔ CovariantClass α>0 α (fun x y => y * x) (· ≤ ·) :=
  ⟨@MulPosMono.to_covariantClass_pos_mul_le _ _ _ _, fun h =>
    {
      elim a b c
        h := by
        obtain ha | ha := a.prop.eq_or_lt
        · simp [← ha]
        · exact @CovariantClass.elim α>0 α (fun x y => y * x) (· ≤ ·) _ ⟨_, ha⟩ _ _ h }⟩

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