himp_ne_right

Mathlib.Order.BooleanAlgebra.Basic

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

English

In a Boolean algebra, x ⇨ y ≠ x iff x ≠ ⊤ or y ≠ ⊤.

Русский

В булевой алгебре x ⇨ y ≠ x эквивалентно x ≠ ⊤ или y ≠ ⊤.

LaTeX

$$x \Rightarrow y \neq x \;\iff\; x \neq \top \;\lor\; y \neq \top$$

Lean4

theorem himp_ne_right : x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤ :=
  himp_eq_left.not.trans not_and_or

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

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

Разделы

Аффилиация

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