refl

Mathlib.Analysis.Convex.Exposed

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

← MathLib Explorer

English

Any set A is exposed in itself: IsExposed 𝕜 A A.

Русский

Любое множество A экспонировано относительно самого себя: IsExposed 𝕜 A A.

LaTeX

$$$\\mathrm{IsExposed}\\ 𝕜\\ A\\ A$$$

Lean4

@[refl]
protected theorem refl (A : Set E) : IsExposed 𝕜 A A := fun ⟨_, _⟩ =>
  ⟨0, Subset.antisymm (fun _ hx => ⟨hx, fun _ _ => le_refl 0⟩) fun _ hx => hx.1⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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