add_mem

Mathlib.Geometry.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#ConvexCone.add_mem

English

If x ∈ C and y ∈ C, then x + y ∈ C.

Русский

Если x ∈ C и y ∈ C, то x + y ∈ C.

LaTeX

$$$x \\in C \\land y \\in C \\Rightarrow x + y \\in C$$$

Lean4

protected theorem add_mem ⦃x⦄ (hx : x ∈ C) ⦃y⦄ (hy : y ∈ C) : x + y ∈ C :=
  C.add_mem' hx hy

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru