to_isOrderedAddMonoid — Mathlib

English

A blunt cone is salient.

Русский

Тупой конус заметен.

LaTeX

$$C.Blunt \rightarrow C.Salient$$

Lean4

/-- A pointed and salient cone defines an `IsOrderedAddMonoid`. -/
theorem to_isOrderedAddMonoid (C : ConvexCone R G) (h₁ : C.Pointed) (h₂ : C.Salient) :
    let _ := toPartialOrder C h₁ h₂
    IsOrderedAddMonoid G :=
  let _ := toPartialOrder C h₁ h₂
  {
    add_le_add_left := by
      intro a b hab c
      change c + b - (c + a) ∈ C
      rw [add_sub_add_left_eq_sub]
      exact hab }

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