sub

Mathlib.Analysis.Convex.Basic

URI: https://scilib.ai/kg/mathlib#Convex.sub

English

The difference of two convex sets is convex.

Русский

Разность выпуклых множеств выпукла.

LaTeX

$$$$ \\operatorname{Convex}_{\\mathbb{K}}(s - t) $$$$

Lean4

theorem sub (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s - t) :=
  by
  rw [sub_eq_add_neg]
  exact hs.add ht.neg

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

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

Разделы

Аффилиация

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