le_sdiff_of_le_left

Mathlib.Order.Heyting.Basic

URI: https://scilib.ai/kg/mathlib#Disjoint.le_sdiff_of_le_left

← MathLib Explorer

English

If a ⊥ c and a ≤ b, then a ≤ b \ c.

Русский

Пусть Disjoint(a,c) и a ≤ b; тогда a ≤ b \ c.

LaTeX

$$$ (A \subseteq B) \land (A \cap C = \emptyset) \Rightarrow (A \subseteq B \setminus C) $$$

Lean4

/-- See `le_sdiff` for a stronger version in generalised Boolean algebras. -/
theorem le_sdiff_of_le_left (hac : Disjoint a c) (hab : a ≤ b) : a ≤ b \ c :=
  hac.sdiff_eq_left.ge.trans <| sdiff_le_sdiff_right hab

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

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

Разделы

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

Аффилиация

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