sdiff_sdiff_sdiff_cancel_right

Mathlib.Order.BooleanAlgebra.Basic

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

← MathLib Explorer

English

(x \ z) \ (y \ z) = x \ y.

Русский

(x \ z) \ (y \ z) = x \ y.

LaTeX

$$$$ (x \setminus z) \setminus (y \setminus z) = x \setminus y $$$$

Lean4

theorem sdiff_sdiff_sdiff_cancel_right (hcb : z ≤ y) : (x \ z) \ (y \ z) = x \ y :=
  by
  rw [le_antisymm_iff, sdiff_le_comm]
  exact
    ⟨sdiff_sdiff_sdiff_le_sdiff,
      (disjoint_sdiff_self_left.mono_right sdiff_le).le_sdiff_of_le_left <| sdiff_le_sdiff_left hcb⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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