mtr

Mathlib.Logic.Basic

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

English

If (¬a → ¬b) and b hold, then a holds: (¬a → ¬b) → b → a.

Русский

Если (¬a → ¬b) и b истина, тогда a истина: (¬a → ¬b) → b → a.

LaTeX

$$$(\\neg a \\to \\neg b) \\to b \\to a$$$

Lean4

/-- Provide the reverse of modus tollens (`mt`) as dot notation for implications. -/
protected theorem mtr : (¬a → ¬b) → b → a :=
  not_imp_not.mp

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

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

Разделы

Аффилиация

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