sSup_eq

Mathlib.Order.Partition.Basic

URI: https://scilib.ai/kg/mathlib#Partition.sSup_eq

English

There is a natural equivalence between the subtype of blocks of P.copy hst and the subtype of blocks of P.

Русский

Существует естественное эквивалентность между подтипом блоков P.copy hst и подтипом блоков P.

LaTeX

$$$(P.copy\;hst)\;\simeq\; P$$$

Lean4

@[simp]
theorem sSup_eq (P : Partition s) : sSup P = s :=
  P.sSup_eq'

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

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

Разделы

Аффилиация

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