eq

Mathlib.Combinatorics.SetFamily.Compression.UV

URI: https://scilib.ai/kg/mathlib#UV.IsCompressed.eq

English

If a triple (u, v, s) is compressed, then applying the compression to s yields s itself; i.e., the compression does not change s when IsCompressed holds.

Русский

Если тройка (u, v, s) сжата, то сжатие s по этим параметрам возвращает сам s; тождественность сжатия.

LaTeX

$$$\\mathcal{C}_{u,v}(s) = s$$$

Lean4

protected theorem eq (h : IsCompressed u v s) : 𝓒 u v s = s :=
  h

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

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

Разделы

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

Аффилиация

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