sdiff_top

Mathlib.Order.Heyting.Basic

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

English

For every a in a co-Heyting algebra, the left residual of a by the top element is the bottom: a \ ⊤ = ⊥.

Русский

Для каждого a в ко-эйтинговой алгебре левый остаток a по верхнему элементу равен нижнему: a \ ⊤ = ⊥.

LaTeX

$$$$ a \top = \bot $$$$

Lean4

@[simp]
theorem sdiff_top (a : α) : a \ ⊤ = ⊥ :=
  sdiff_eq_bot_iff.2 le_top

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

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

Разделы

Аффилиация

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