disjoint_iff

Mathlib.Order.PropInstances

URI: https://scilib.ai/kg/mathlib#Prop.disjoint_iff

English

For propositions P and Q, Disjoint P Q is equivalent to not (P and Q).

Русский

Для пропозиций P и Q дизjoint-произвольно эквивалентен не (P и Q).

LaTeX

$$$\mathrm{Disjoint}(P,Q) \ \iff \ \neg(P \land Q).$$$

Lean4

@[simp]
theorem disjoint_iff {P Q : Prop} : Disjoint P Q ↔ ¬(P ∧ Q) :=
  disjoint_iff_inf_le

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

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

Разделы

Аффилиация

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