coe

Mathlib.Order.Partition.Basic

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

English

The map sending a partition P to its underlying set is the canonical projection.

Русский

Отображение, отправляющее разбиение P в его основанное множество, является канонической проекцией.

LaTeX

$$$\mathrm{coe}\,(P) = P$$$

Lean4

/-- See Note [custom simps projection]. -/
def coe {s : α} (P : Partition s) : Set α :=
  P

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

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

Разделы

Аффилиация

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