sdiff_sdiff_le

Mathlib.Order.Heyting.Basic

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

English

For all a,b,c, a \ (a \ b) ≤ b.

Русский

Для всех a,b,c выполняется a \ (a \ b) ≤ b.

LaTeX

$$$ a \ (a \setminus b) \le b $$$

Lean4

theorem sdiff_sdiff_le : a \ (a \ b) ≤ b :=
  sdiff_le_iff.2 le_sdiff_sup

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

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

Разделы

Аффилиация

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