Ici_bot

Mathlib.Order.Interval.Finset.Basic

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

English

If a bottom exists, Ici(bottom) equals univ.

Русский

Если существует нижняя граница, то Ici(нило) равно единице.

LaTeX

$$$ Ici(\bot) = univ $$$

Lean4

@[simp]
theorem Ici_bot [OrderBot α] [Fintype α] : Ici (⊥ : α) = univ := by ext a; simp only [mem_Ici, bot_le, mem_univ]

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

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

Разделы

Аффилиация

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