le_sdiff_iff

Mathlib.Order.CompleteBooleanAlgebra

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

English

For a frame, a ≤ b \ c is equivalent to: for all d, if b ≤ c ⊔ d then a ≤ d.

Русский

Для рамки: a ≤ b \ c эквивалентно: для всех d, если b ≤ c ⊔ d, тогда a ≤ d.

LaTeX

$$$a \le b \setminus c \iff \forall d,\; b \le c \lor d \Rightarrow a \le d$$$

Lean4

theorem le_sdiff_iff : a ≤ b \ c ↔ ∀ d, b ≤ c ⊔ d → a ≤ d := by
  simp [sdiff_eq_sInf]
    -- see Note [lower instance priority]

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

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

Разделы

Аффилиация

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