sdiff_le_inf_hnot

Mathlib.Order.Heyting.Basic

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

English

For all a,b in a co-Heyting algebra, the left residual a \ b is below a ∧ ¬b: a \ b ≤ a ∧ ¬b.

Русский

Для всех a,b в коэйтинговой алгебре левый остаток a \ b ниже a ∧ ¬b.

LaTeX

$$$$ a \ b \le a \land \neg b $$$$

Lean4

theorem sdiff_le_inf_hnot : a \ b ≤ a ⊓ ￢b :=
  le_inf sdiff_le sdiff_le_hnot

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

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

Разделы

Аффилиация

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