le_sdiff_right

Mathlib.Order.BooleanAlgebra.Basic

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

← MathLib Explorer

English

For hz : z ≤ y and hx : x ≤ y, x ≤ z iff Disjoint z (y \ x).

Русский

Пусть z ≤ y и x ≤ y. Тогда x ≤ z если и только если Disjoint z (y \ x).

LaTeX

$$$hz : z \le y \land hx : x \le y \Rightarrow x \le z \iff Disjoint z (y \setminus x)$$$

Lean4

@[simp]
theorem le_sdiff_right : x ≤ y \ x ↔ x = ⊥ :=
  ⟨fun h => disjoint_self.1 (disjoint_sdiff_self_right.mono_right h), fun h => h.le.trans bot_le⟩

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

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

Разделы

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

Аффилиация

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