imp_and_neg_imp_iff

Mathlib.Logic.Basic

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

English

(p → q) ∧ (¬p → q) ↔ q.

Русский

(p → q) и (¬p → q) эквивалентно q.

LaTeX

$$$((p \rightarrow q) \land (\\neg p \rightarrow q)) \\leftrightarrow q$$$

Lean4

theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q := by simp

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

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

Разделы

Аффилиация

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