inf_sdiff_sup_left

Mathlib.Order.Heyting.Basic

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

English

For all α with a generalized co-Heyting algebra structure, (a \\ c) ⊓ (a ⊔ b) = a \\ c.

Русский

Для любого a в обобщённой коейтинговой алгебре: (a \\ c) ⊓ (a ⊔ b) = a \\ c.

LaTeX

$$$ (a \\\\setminus c) \\\\sqcap (a \\\\vee b) = a \\\\setminus c $$$

Lean4

@[simp]
theorem inf_sdiff_sup_left : a \ c ⊓ (a ⊔ b) = a \ c :=
  inf_of_le_left <| sdiff_le.trans le_sup_left

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

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

Разделы

Аффилиация

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