Contrapose
📁 Source: Mathlib/Tactic/Contrapose.lean
Statistics
| Metric | Count |
|---|---|
| 3 | |
| 8 | |
| Total | 11 |
Mathlib.Tactic.Contrapose
Definitions
| Name | Category | Theorems |
|---|---|---|
contrapose 📖 | CompOp | — |
contrapose! 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
contrapose_iff₁ 📖 | — | — | — | — | not_iff_not |
contrapose_iff₂ 📖 | — | — | — | — | iff_not_comm |
contrapose_iff₃ 📖 | — | — | — | — | not_iff_comm |
contrapose_iff₄ 📖 | — | — | — | — | — |
contrapose₁ 📖 | — | — | — | — | by_contra |
contrapose₂ 📖 | — | — | — | — | by_contra |
contrapose₃ 📖 | — | — | — | — | Imp.swap |
contrapose₄ 📖 | — | — | — | — | — |
Mathlib.Tactic.Contrapose.contrapose
Definitions
| Name | Category | Theorems |
|---|---|---|
negate_iff 📖 | CompOp | — |
---