bot_lt_Iic

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#LowerSet.bot_lt_Iic

English

The bottom element is strictly less than the principal lower set Iic a for any a.

Русский

Нижний элемент строго меньше соответствующего нижнего множества Iic a для любого a.

LaTeX

$$$\bot < Iic a$$$

Lean4

@[simp]
theorem bot_lt_Iic : ⊥ < Iic a :=
  bot_lt_iff_ne_bot.2 Iic_ne_bot

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

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

Разделы

Аффилиация

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