sdiff_bot

Mathlib.Order.Heyting.Basic

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

English

Same as previous bound: (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_bot : a \ ⊥ = a :=
  eq_of_forall_ge_iff fun b => by rw [sdiff_le_iff, bot_sup_eq]

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

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

Разделы

Аффилиация

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