mulPosReflectLT_iff_contravariant_pos

English

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

Русский

MulPosReflectLT α эквивалентно ContravariantClass α>0 α (переменная справа) (<).

LaTeX

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

Lean4

theorem mulPosReflectLT_iff_contravariant_pos :
    MulPosReflectLT α ↔ ContravariantClass α>0 α (fun x y => y * x) (· < ·) :=
  ⟨@MulPosReflectLT.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 => y * x) (· < ·) _ ⟨_, ha⟩ _ _ h }⟩
    -- see Note [lower instance priority]

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