sdiff_eq_symm

Mathlib.Order.BooleanAlgebra.Basic

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

English

If hy ≤ x and x \ y = z, then x \ z = y.

Русский

Если y ≤ x и x \ y = z, то x \ z = y.

LaTeX

$$$$ y \le x \Rightarrow x \setminus y = z \Rightarrow x \setminus z = y $$$$

Lean4

theorem sdiff_eq_symm (hy : y ≤ x) (h : x \ y = z) : x \ z = y := by rw [← h, sdiff_sdiff_eq_self hy]

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

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

Разделы

Аффилиация

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