le_isTotal

Mathlib.Order.PropInstances

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

English

For any propositions P and Q, either P implies Q or Q implies P.

Русский

Для любых пропозиций P и Q выполняется либо P ⇒ Q, либо Q ⇒ P.

LaTeX

$$$\forall P,Q \in \mathrm{Prop},\ P \to Q \lor Q \to P$$$

Lean4

instance le_isTotal : IsTotal Prop (· ≤ ·) :=
  ⟨fun p q => by by_cases h : q <;> simp [h]⟩

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

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

Разделы

Аффилиация

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