and_or_imp

Mathlib.Logic.Basic

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

English

The formula a ∧ b ∨ (a → c) is equivalent to a → (b ∨ c).

Русский

Формула a ∧ b ∨ (a → c) эквивалентна a → (b ∨ c).

LaTeX

$$$ a \\wedge b \\lor (a \\rightarrow c) \\leftrightarrow a \\rightarrow (b \\lor c). $$$

Lean4

theorem and_or_imp {a b c : Prop} : a ∧ b ∨ (a → c) ↔ a → b ∨ c :=
  open scoped Classical in Decidable.and_or_imp

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

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

Разделы

Аффилиация

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