toPreorder — Mathlib

English

A pointed and salient cone defines a preorder on G by x ≤ y iff y − x ∈ C.

Русский

Ориентированный и заметный конус определяет преформу на G: x ≤ y если y − x ∈ C.

LaTeX

$$def toPreorder (C) (h₁) (h₂) : Preorder G := ... le x y := y - x ∈ C$$

Lean4

/-- A pointed convex cone defines a preorder. -/
def toPreorder (C : ConvexCone R G) (h₁ : C.Pointed) : Preorder G
    where
  le x y := y - x ∈ C
  le_refl x := by rw [sub_self x]; exact h₁
  le_trans x y z xy zy := by simpa using add_mem zy xy

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