imp_iff_or_not

Mathlib.Logic.Basic

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

English

b → a is equivalent to a ∨ ¬b.

Русский

b → a эквивалентно a ∨ ¬b.

LaTeX

$$$b \rightarrow a \leftrightarrow (a \\lor \\neg b)$$$

Lean4

theorem imp_iff_or_not {b a : Prop} : b → a ↔ a ∨ ¬b :=
  open scoped Classical in Decidable.imp_iff_or_not

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

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

Разделы

Аффилиация

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