antisymm

Mathlib.Analysis.Convex.Exposed

URI: https://scilib.ai/kg/mathlib#IsExposed.antisymm

English

If A is exposed in B and B is exposed in A, then A equals B.

Русский

Если A экспонирована в B и B экспонирована в A, то A = B.

LaTeX

$$$\\mathrm{IsExposed}\\ 𝕜\\ A\\ B \\to \\mathrm{IsExposed}\\ 𝕜\\ B\\ A \\Rightarrow A = B$$$

Lean4

protected theorem antisymm (hB : IsExposed 𝕜 A B) (hA : IsExposed 𝕜 B A) : A = B :=
  hA.subset.antisymm hB.subset

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

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

Разделы

Аффилиация

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