sdiff_eq_comm

Mathlib.Order.BooleanAlgebra.Basic

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

English

For hy ≤ x and hz ≤ x, x \ y = z is equivalent to x \ z = y.

Русский

При hy ≤ x и hz ≤ x равносильно x \ y = z ⇔ x \ z = y.

LaTeX

$$$$ y \le x \land z \le x \Rightarrow (x \setminus y = z) \iff (x \setminus z = y) $$$$

Lean4

theorem sdiff_eq_comm (hy : y ≤ x) (hz : z ≤ x) : x \ y = z ↔ x \ z = y :=
  ⟨sdiff_eq_symm hy, sdiff_eq_symm hz⟩

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

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

Разделы

Аффилиация

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