Logic
📁 Source: Batteries/Logic.lean
Statistics
Classical
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
exists_not_of_not_forall 📖 | — | — | — | — | — |
Decidable
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
exists_not_of_not_forall 📖 | — | — | — | — | — |
Eq
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
congr_left 📖 | — | — | — | — | — |
congr_right 📖 | — | — | — | — | — |
Function
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
id_def 📖 | — | — | — | — | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
instDecidablePredComp_batteries 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
cast_eq_iff_heq 📖 | — | — | — | — | heq_of_cast_eq |
congrArg₂ 📖 | — | — | — | — | — |
congrFun₂ 📖 | — | — | — | — | — |
congrFun₃ 📖 | — | — | — | — | congrFun₂ |
congr_arg 📖 | — | — | — | — | — |
congr_arg₂ 📖 | — | — | — | — | congrArg₂ |
congr_eqRec 📖 | — | — | — | — | — |
congr_fun 📖 | — | — | — | — | — |
congr_fun₂ 📖 | — | — | — | — | congrFun₂ |
congr_fun₃ 📖 | — | — | — | — | congrFun₃ |
eqRec_eq_cast 📖 | — | — | — | — | — |
eqRec_heq_iff_heq 📖 | — | — | — | — | — |
eqRec_heq_self 📖 | — | — | — | — | — |
eq_rec_constant 📖 | — | — | — | — | — |
funext₂ 📖 | — | — | — | — | — |
funext₃ 📖 | — | — | — | — | funext₂ |
heq_eqRec_iff_heq 📖 | — | — | — | — | — |
heq_iff_eq 📖 | — | — | — | — | — |
heq_of_cast_eq 📖 | — | — | — | — | — |
not_nonempty_empty 📖 | — | — | — | — | — |
not_nonempty_pempty 📖 | — | — | — | — | — |
subsingleton_iff_forall_eq 📖 | — | — | — | — | subsingleton_of_forall_eq |
subsingleton_of_forall_eq 📖 | — | — | — | — | — |
---