disjoint_bot_left

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#disjoint_bot_left

English

Bottom is disjoint from any element on the left side: Disjoint(⊥, a).

Русский

Нижняя грань диссоциируется с любым элементом слева: Disjoint(⊥, a).

LaTeX

$$$Disjoint(\\bot, a)$$$

Lean4

@[simp]
theorem disjoint_bot_left : Disjoint ⊥ a := fun _ hbot _ ↦ hbot

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

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

Разделы

Аффилиация

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