by_contradiction

Mathlib.Logic.Basic

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

English

From ¬p → False, deduce p.

Русский

Из ¬p → False следует p.

LaTeX

$$$(\neg p \to \bot) \to p$$$

Lean4

theorem by_contradiction {p : Prop} : (¬p → False) → p :=
  open scoped Classical in Decidable.byContradiction

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

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

Разделы

Аффилиация

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