Theorems

📁 Source: Mathlib/Tactic/FunProp/Theorems.lean

Statistics

Metric	Count
Definitions `FunctionTheorem`, `appliedArgs`, `form`, `funOrigin`, `funPropName`, `getProof`, `mainArgs`, `priority`, `thmOrigin`, `FunctionTheorems`, `theorems`, `FunctionTheoremsExt`, `getProof`, `GeneralTheoremsExt`, `LambdaTheorem`, `funPropName`, `getProof`, `thmArgs`, `thmName`, `LambdaTheoremArgs`, `type`, `LambdaTheoremType`, `LambdaTheorems`, `theorems`, `LambdaTheoremsExt`, `Theorem`, `TheoremForm`, `addTheorem`, `detectLambdaTheoremArgs`, `functionTheoremsExt`, `getLambdaTheorems`, `getMorphismTheorems`, `getTheoremFromConst`, `getTheoremsForFunction`, `getTransitionTheorems`, `instBEqFunctionTheorem`, `beq`, `instBEqLambdaTheorem`, `beq`, `instBEqLambdaTheoremArgs`, `beq`, `instBEqLambdaTheoremType`, `beq`, `instBEqTheoremForm`, `beq`, `instHashableLambdaTheoremArgs`, `hash`, `instHashableLambdaTheoremType`, `hash`, `instInhabitedFunctionTheorem`, `default`, `instInhabitedFunctionTheorems`, `default`, `instInhabitedLambdaTheorem`, `default`, `instInhabitedLambdaTheoremArgs`, `default`, `instInhabitedLambdaTheoremType`, `default`, `instInhabitedLambdaTheorems`, `default`, `instInhabitedTheoremForm`, `default`, `instReprLambdaTheoremArgs`, `repr`, `instReprLambdaTheoremType`, `repr`, `instReprTheoremForm`, `repr`, `instToStringTheoremForm`, `lambdaTheoremsExt`, `morTheoremsExt`, `transitionTheoremsExt`	73
Theorems	0
Total	73

Mathlib.Meta.FunProp

Definitions

Name	Category	Theorems
`FunctionTheorem` 📖	CompData	—
`FunctionTheorems` 📖	CompData	—
`FunctionTheoremsExt` 📖	CompOp	—
`GeneralTheoremsExt` 📖	CompOp	—
`LambdaTheorem` 📖	CompData	—
`LambdaTheoremArgs` 📖	CompData	—
`LambdaTheoremType` 📖	CompData	—
`LambdaTheorems` 📖	CompData	—
`LambdaTheoremsExt` 📖	CompOp	—
`Theorem` 📖	CompData	—
`TheoremForm` 📖	CompData	—
`addTheorem` 📖	CompOp	—
`detectLambdaTheoremArgs` 📖	CompOp	—
`functionTheoremsExt` 📖	CompOp	—
`getLambdaTheorems` 📖	CompOp	—
`getMorphismTheorems` 📖	CompOp	—
`getTheoremFromConst` 📖	CompOp	—
`getTheoremsForFunction` 📖	CompOp	—
`getTransitionTheorems` 📖	CompOp	—
`instBEqFunctionTheorem` 📖	CompOp	—
`instBEqLambdaTheorem` 📖	CompOp	—
`instBEqLambdaTheoremArgs` 📖	CompOp	—
`instBEqLambdaTheoremType` 📖	CompOp	—
`instBEqTheoremForm` 📖	CompOp	—
`instHashableLambdaTheoremArgs` 📖	CompOp	—
`instHashableLambdaTheoremType` 📖	CompOp	—
`instInhabitedFunctionTheorem` 📖	CompOp	—
`instInhabitedFunctionTheorems` 📖	CompOp	—
`instInhabitedLambdaTheorem` 📖	CompOp	—
`instInhabitedLambdaTheoremArgs` 📖	CompOp	—
`instInhabitedLambdaTheoremType` 📖	CompOp	—
`instInhabitedLambdaTheorems` 📖	CompOp	—
`instInhabitedTheoremForm` 📖	CompOp	—
`instReprLambdaTheoremArgs` 📖	CompOp	—
`instReprLambdaTheoremType` 📖	CompOp	—
`instReprTheoremForm` 📖	CompOp	—
`instToStringTheoremForm` 📖	CompOp	—
`lambdaTheoremsExt` 📖	CompOp	—
`morTheoremsExt` 📖	CompOp	—
`transitionTheoremsExt` 📖	CompOp	—

Mathlib.Meta.FunProp.FunctionTheorem

Definitions

Name	Category	Theorems
`appliedArgs` 📖	CompOp	—
`form` 📖	CompOp	—
`funOrigin` 📖	CompOp	—
`funPropName` 📖	CompOp	—
`getProof` 📖	CompOp	—
`mainArgs` 📖	CompOp	—
`priority` 📖	CompOp	—
`thmOrigin` 📖	CompOp	—

Mathlib.Meta.FunProp.FunctionTheorems

Definitions

Name	Category	Theorems
`theorems` 📖	CompOp	—

Mathlib.Meta.FunProp.GeneralTheorem

Definitions

Name	Category	Theorems
`getProof` 📖	CompOp	—

Mathlib.Meta.FunProp.LambdaTheorem

Definitions

Name	Category	Theorems
`funPropName` 📖	CompOp	—
`getProof` 📖	CompOp	—
`thmArgs` 📖	CompOp	—
`thmName` 📖	CompOp	—

Mathlib.Meta.FunProp.LambdaTheoremArgs

Definitions

Name	Category	Theorems
`type` 📖	CompOp	—

Mathlib.Meta.FunProp.LambdaTheorems

Definitions

Name	Category	Theorems
`theorems` 📖	CompOp	—

Mathlib.Meta.FunProp.instBEqFunctionTheorem

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Mathlib.Meta.FunProp.instBEqLambdaTheorem

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Mathlib.Meta.FunProp.instBEqLambdaTheoremType

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Mathlib.Meta.FunProp.instBEqTheoremForm

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs

Definitions

Name	Category	Theorems
`hash` 📖	CompOp	—

Mathlib.Meta.FunProp.instHashableLambdaTheoremType

Definitions

Name	Category	Theorems
`hash` 📖	CompOp	—

Mathlib.Meta.FunProp.instInhabitedFunctionTheorem

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Meta.FunProp.instInhabitedFunctionTheorems

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Meta.FunProp.instInhabitedLambdaTheorem

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Meta.FunProp.instInhabitedLambdaTheorems

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Meta.FunProp.instInhabitedTheoremForm

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Meta.FunProp.instReprLambdaTheoremArgs

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

Mathlib.Meta.FunProp.instReprLambdaTheoremType

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

Mathlib.Meta.FunProp.instReprTheoremForm

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

---

← Back to Index