codisjoint_himp_self_right

Mathlib.Order.BooleanAlgebra.Basic

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

English

Codisjoint x (x ⇨ y) holds in a Boolean algebra.

Русский

Codisjoint x (x ⇨ y) выполняется в булевой алгебре.

LaTeX

$$Codisjoint x (x \Rightarrow y)$$

Lean4

theorem codisjoint_himp_self_right : Codisjoint x (x ⇨ y) :=
  @disjoint_sdiff_self_right αᵒᵈ _ _ _

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

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

Разделы

Аффилиация

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