instZero — Mathlib

English

There exists a zero element in the space of convex bodies: the one whose underlying set is {0} centered at 0, which is convex, compact, and nonempty.

Русский

Существуют нуль-элемент в пространстве выпуклых тел: тело, основанное на множества {0}, выпукло, компактно и ненулево.

LaTeX

$$$$ 0_{\\mathrm{ConvexBody}(V)} = \\langle 0,\\ \\mathrm{convex\\_singleton}(0),\\ \\mathrm{isCompact\\_singleton},\\ \\mathrm{Set.singleton\\_nonempty}(0)\\rangle. $$$$

Lean4

instance : Zero (ConvexBody V) where zero := ⟨0, convex_singleton 0, isCompact_singleton, Set.singleton_nonempty 0⟩

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