posMulMono_iff_covariant_pos — Mathlib

English

PosMulMono α is equivalent to CovariantClass α>0 α (×) (≤).

Русский

PosMulMono α эквивалентно CovariantClass α>0 α (×) (≤).

LaTeX

$$$$ PosMulMono \alpha \ \Longleftrightarrow \ CovariantClass \alpha>0 \alpha (\cdot) (\le). $$$$

Lean4

theorem posMulMono_iff_covariant_pos : PosMulMono α ↔ CovariantClass α>0 α (fun x y => x * y) (· ≤ ·) :=
  ⟨@PosMulMono.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 => x * y) (· ≤ ·) _ ⟨_, ha⟩ _ _ h }⟩

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