eq_of_sdiff_eq_sdiff

Mathlib.Order.BooleanAlgebra.Basic

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

← MathLib Explorer

English

If hxz: x ≤ z, hyz: y ≤ z, and z \ x = z \ y, then x = y.

Русский

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

LaTeX

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

Lean4

theorem eq_of_sdiff_eq_sdiff (hxz : x ≤ z) (hyz : y ≤ z) (h : z \ x = z \ y) : x = y := by
  rw [← sdiff_sdiff_eq_self hxz, h, sdiff_sdiff_eq_self hyz]

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

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

Разделы

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

Аффилиация

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