toPartialOrder — Mathlib

English

If C1 ≤ C2 and C1 is pointed, then C2 is pointed.

Русский

Если C1 ⊆ C2 и C1 указательный, то и C2 указательный.

LaTeX

$$ (h : C_1 ≤ C_2) → (C_1.Pointed → C_2.Pointed)$$

Lean4

/-- A pointed and salient cone defines a partial order. -/
def toPartialOrder (C : ConvexCone R G) (h₁ : C.Pointed) (h₂ : C.Salient) : PartialOrder G :=
  { toPreorder C h₁ with
    le_antisymm := by
      intro a b ab ba
      by_contra h
      have h' : b - a ≠ 0 := fun h'' => h (eq_of_sub_eq_zero h'').symm
      have H := h₂ (b - a) ab h'
      rw [neg_sub b a] at H
      exact H ba }

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