sdiff_ne_right

Mathlib.Order.BooleanAlgebra.Basic

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

English

x \ y ≠ y if and only if x ≠ ⊥ or y ≠ ⊥.

Русский

x \ y ≠ y тогда и только тогда, когда x ≠ ⊥ или y ≠ ⊥.

LaTeX

$$$x \setminus y \neq y \iff x \neq \bot \lor y \neq \bot$$$

Lean4

theorem sdiff_ne_right : x \ y ≠ y ↔ x ≠ ⊥ ∨ y ≠ ⊥ :=
  sdiff_eq_right.not.trans not_and_or

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

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

Разделы

Аффилиация

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