Flat — Mathlib

English

A convex cone is flat if it contains some nonzero vector x and its opposite −x.

Русский

Выпуклый конус плоский, если в нем содержится некоторый ненулевой вектор x и его противоположность −x.

LaTeX

$$ConvexCone.Flat (C) : ∃ x ∈ C, x ≠ (0 : G) ∧ -x ∈ C$$

Lean4

/-- A convex cone is flat if it contains some nonzero vector `x` and its opposite `-x`. -/
def Flat (C : ConvexCone R G) : Prop :=
  ∃ x ∈ C, x ≠ (0 : G) ∧ -x ∈ C

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