posMulReflectLT_iff_contravariant_pos

English

PosMulReflectLT α is equivalent to ContravariantClass α>0 α (fun x y => x * y) (<).

Русский

PosMulReflectLT α эквивалентно ContravariantClass α>0 α (умножение слева) (<).

LaTeX

$$$$ PosMulReflectLT \alpha \Longleftrightarrow ContravariantClass \alpha>0 \alpha (fun x y => x \cdot y) (<). $$$$

Lean4

theorem posMulReflectLT_iff_contravariant_pos :
    PosMulReflectLT α ↔ ContravariantClass α>0 α (fun x y => x * y) (· < ·) :=
  ⟨@PosMulReflectLT.to_contravariantClass_pos_mul_lt _ _ _ _, fun h =>
    {
      elim a b c
        h := by
        obtain ha | ha := a.prop.eq_or_lt
        · simp [← ha] at h
        · exact @ContravariantClass.elim α>0 α (fun x y => x * y) (· < ·) _ ⟨_, ha⟩ _ _ h }⟩

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