sSupIndep

Mathlib.Order.Partition.Basic

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

English

A partition P of s is sSupIndep as a subset of α.

Русский

Разбиение P s является независимым относительно sSup в подмножестве α.

LaTeX

$$$P\,:\; sSupIndep\,(P\;:\; Set\;\alpha)$$$

Lean4

@[simp]
theorem sSupIndep (P : Partition s) : sSupIndep (P : Set α) :=
  P.sSupIndep'

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

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

Разделы

Аффилиация

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