bot_mem_insertBot

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#WithBot.bot_mem_insertBot

English

The bottom element ⊥ belongs to insertBot s for any finite set s.

Русский

Нижний элемент ⊥ принадлежит insertBot s для любого конечного множества s.

LaTeX

$$$ \bot \in insertBot(s) $$$

Lean4

@[simp]
theorem bot_mem_insertBot {s : Finset α} : ⊥ ∈ insertBot s := by simp [insertBot]

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

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

Разделы

Аффилиация

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