coe

Mathlib.Topology.Sets.Compacts

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Compacts.Simps.coe

English

The Simps projection on Compacts α is simply the underlying set of a compact subset.

Русский

Проекция Simps на Compacts α просто задаёт подмножество как множество.

LaTeX

$$$\mathrm{coe}(s) = s.$$$

Lean4

/-- See Note [custom simps projection]. -/
def coe (s : Compacts α) : Set α :=
  s

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

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

Разделы

Аффилиация

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