sdiff_self

Mathlib.Order.Heyting.Basic

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

English

In a generalized co-Heyting algebra, a \\ a equals bottom.

Русский

В обобщенной коейтинговой алгебре a \\ a равно нулю.

LaTeX

$$$a \\setminus a = \\bot$$$

Lean4

@[simp]
theorem sdiff_self : a \ a = ⊥ :=
  le_bot_iff.1 <| sdiff_le_iff.2 le_sup_left

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

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

Разделы

Аффилиация

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