mtr

Mathlib.Tactic.Contrapose

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Contrapose.mtr

Lean4

theorem mtr {p q : Prop} : (¬q → ¬p) → (p → q) := fun h hp ↦ by_contra (fun h' ↦ h h' hp)

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

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

Разделы

Аффилиация

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