mt

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#Function.mt

English

Modus tollens: from a → b and ¬b we deduce ¬a.

Русский

Модус толленс: из a → b и ¬b следует ¬a.

LaTeX

$$$ \\text{Function}.mt: (a \\rightarrow b) \\rightarrow \\lnot b \\rightarrow \\lnot a. $$$

Lean4

/-- Provide modus tollens (`mt`) as dot notation for implications. -/
protected theorem mt {a b : Prop} : (a → b) → ¬b → ¬a :=
  mt

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

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

Разделы

Аффилиация

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