codisjoint_himp_self_left

Mathlib.Order.BooleanAlgebra.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem codisjoint_himp_self_left : Codisjoint (x ⇨ y) x :=
  @disjoint_sdiff_self_left αᵒᵈ _ _ _

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

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

Разделы

Аффилиация

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