instSetLike — Mathlib

English

The underlying set of a convex body is a convex subset of V; equivalently, for any x, y in K and t in [0,1], the point t x + (1-t) y lies in K.

Русский

Множество, лежащее внутри выпуклого тела, выпукло: для любых x, y в K и для всех t ∈ [0,1] имеет место t x + (1-t) y ∈ K.

LaTeX

$$$\forall x,y \in K, \ \forall t \in [0,1],\ \ t x + (1-t) y \in K$$$

Lean4

instance : SetLike (ConvexBody V) V where
  coe := ConvexBody.carrier
  coe_injective' K L
    h := by
    cases K
    cases L
    congr

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