isCompl_iff

Mathlib.Order.PropInstances

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

← MathLib Explorer

English

IsCompl P Q is equivalent to not (P ↔ Q).

Русский

IsCompl P Q эквивалентно не (P экв Q).

LaTeX

$$$\mathrm{IsCompl}(P,Q) \ \iff \ \neg(P \leftrightarrow Q).$$$

Lean4

@[simp]
theorem isCompl_iff {P Q : Prop} : IsCompl P Q ↔ ¬(P ↔ Q) :=
  by
  rw [_root_.isCompl_iff, «Prop».disjoint_iff, «Prop».codisjoint_iff, not_iff]
  by_cases P <;> by_cases Q <;> simp [*]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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