coe_bot

Mathlib.Combinatorics.Young.YoungDiagram

URI: https://scilib.ai/kg/mathlib#YoungDiagram.coe_bot

English

The underlying set of the bottom diagram is empty.

Русский

Множество, лежащее внизу диаграммы, пусто.

LaTeX

$$$ \uparrow(\bot) = \varnothing. $$$

Lean4

@[norm_cast]
theorem coe_bot : (⊥ : YoungDiagram) = (∅ : Set (ℕ × ℕ)) := by ext; simp

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

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

Разделы

Аффилиация

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