sdiff_eq_bot_iff

Mathlib.Order.Heyting.Basic

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

English

(a \\ b) \\ (a \\ c) ≤ c \\ b.

Русский

(a \\ b) \\ (a \\ c) ≤ c \\ b.

LaTeX

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

Lean4

@[simp]
theorem sdiff_eq_bot_iff : a \ b = ⊥ ↔ a ≤ b := by rw [← le_bot_iff, sdiff_le_iff, sup_bot_eq]

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

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

Разделы

Аффилиация

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