shatterer_idem

Mathlib.Combinatorics.SetFamily.Shatter

URI: https://scilib.ai/kg/mathlib#Finset.shatterer_idem

English

Applying the shatterer operation twice yields the same as applying it once: 𝒜.shatterer.shatterer = 𝒜.shatterer.

Русский

Повторное применение операции шаттерирования не меняет результат: 𝒜.shatterer.shatterer = 𝒜.shatterer.

LaTeX

$$$𝒜.shatterer.shatterer = 𝒜.shatterer$$$

Lean4

@[simp]
theorem shatterer_idem : 𝒜.shatterer.shatterer = 𝒜.shatterer := by simp

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

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

Разделы

Аффилиация

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