Lean4
/-- There are four types of theorems:
- lam - theorem about basic lambda calculus terms
- function - theorem about a specific function(declared or free variable) in specific arguments
- mor - special theorems talking about bundled morphisms/DFunLike.coe
- transition - theorems inferring one function property from another
Examples:
- lam
```
theorem Continuous_id : Continuous fun x => x
theorem Continuous_comp (hf : Continuous f) (hg : Continuous g) : Continuous fun x => f (g x)
```
- function
```
theorem Continuous_add : Continuous (fun x => x.1 + x.2)
theorem Continuous_add (hf : Continuous f) (hg : Continuous g) :
Continuous (fun x => (f x) + (g x))
```
- mor - the head of function body has to be ``DFunLike.code
```
theorem ContDiff.clm_apply {f : E → F →L[𝕜] G} {g : E → F}
(hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
ContDiff 𝕜 n fun x => (f x) (g x)
theorem clm_linear {f : E →L[𝕜] F} : IsLinearMap 𝕜 f
```
- transition - the conclusion has to be in the form `P f` where `f` is a free variable
```
theorem linear_is_continuous [FiniteDimensional ℝ E] {f : E → F} (hf : IsLinearMap 𝕜 f) :
Continuous f
```
-/
inductive Theorem where
| lam (thm : LambdaTheorem)
| function (thm : FunctionTheorem)
| mor (thm : GeneralTheorem)
| transition (thm : GeneralTheorem)
