fun_prop
environment extensions storing theorems for fun_prop
#
Tag for one of the 5 basic lambda theorems, that also hold extra data for composition theorem
- id : LambdaTheoremArgs
Identity theorem e.g.
Continuous fun x => x
- const : LambdaTheoremArgs
Constant theorem e.g.
Continuous fun x => y
- apply : LambdaTheoremArgs
Apply theorem e.g.
Continuous fun (f : (x : X) → Y x => f x)
- comp
(fArgId gArgId : ℕ)
: LambdaTheoremArgs
Composition theorem e.g.
Continuous f → Continuous g → Continuous fun x => f (g x)
The numbers
fArgId
andgArgId
store the argument index forf
andg
in the composition theorem. - pi : LambdaTheoremArgs
Pi theorem e.g.
∀ y, Continuous (f · y) → Continuous fun x y => f x y
Instances For
Tag for one of the 5 basic lambda theorems
- id : LambdaTheoremType
Identity theorem e.g.
Continuous fun x => x
- const : LambdaTheoremType
Constant theorem e.g.
Continuous fun x => y
- apply : LambdaTheoremType
Apply theorem e.g.
Continuous fun (f : (x : X) → Y x => f x)
- comp : LambdaTheoremType
Composition theorem e.g.
Continuous f → Continuous g → Continuous fun x => f (g x)
- pi : LambdaTheoremType
Pi theorem e.g.
∀ y, Continuous (f · y) → Continuous fun x y => f x y
Instances For
Convert LambdaTheoremArgs
to LambdaTheoremType
.
Equations
- Mathlib.Meta.FunProp.LambdaTheoremArgs.id.type = Mathlib.Meta.FunProp.LambdaTheoremType.id
- Mathlib.Meta.FunProp.LambdaTheoremArgs.const.type = Mathlib.Meta.FunProp.LambdaTheoremType.const
- (Mathlib.Meta.FunProp.LambdaTheoremArgs.comp fArgId gArgId).type = Mathlib.Meta.FunProp.LambdaTheoremType.comp
- Mathlib.Meta.FunProp.LambdaTheoremArgs.apply.type = Mathlib.Meta.FunProp.LambdaTheoremType.apply
- Mathlib.Meta.FunProp.LambdaTheoremArgs.pi.type = Mathlib.Meta.FunProp.LambdaTheoremType.pi
Instances For
Decides whether f
is a function corresponding to one of the lambda theorems.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Structure holding information about lambda theorem.
- funPropName : Lean.Name
Name of function property
- thmName : Lean.Name
Name of lambda theorem
- thmArgs : LambdaTheoremArgs
Type and important argument of the theorem.
Instances For
Collection of lambda theorems
- theorems : Std.HashMap (Lean.Name × LambdaTheoremType) (Array LambdaTheorem)
map: function property name × theorem type → lambda theorem
Instances For
Return proof of lambda theorem
Equations
Instances For
Environment extension storing lambda theorems.
Equations
Instances For
Environment extension storing all lambda theorems.
Get lambda theorems for particular function property funPropName
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Function theorems are stated in uncurried or compositional form.
uncurried
theorem Continuous_add : Continuous (fun x => x.1 + x.2)
compositional
theorem Continuous_add (hf : Continuous f) (hg : Continuous g) : Continuous (fun x => (f x) + (g x))
- uncurried : TheoremForm
- comp : TheoremForm
Instances For
Equations
TheoremForm to string
Equations
- One or more equations did not get rendered due to their size.
theorem about specific function (either declared constant or free variable)
- funPropName : Lean.Name
function property name
- thmOrigin : Origin
theorem name
- funOrigin : Origin
function name
array of argument indices about which this theorem is about
- appliedArgs : ℕ
total number of arguments applied to the function
- priority : ℕ
priority
- form : TheoremForm
form of the theorem, see documentation of TheoremForm
Instances For
Equations
- One or more equations did not get rendered due to their size.
- theorems : Std.TreeMap Lean.Name (Std.TreeMap Lean.Name (Array FunctionTheorem) compare) compare
map: function name → function property → function theorem
Instances For
return proof of function theorem
Equations
- thm.getProof = match thm.thmOrigin with | Mathlib.Meta.FunProp.Origin.decl name => Lean.Meta.mkConstWithFreshMVarLevels name | Mathlib.Meta.FunProp.Origin.fvar id => pure (Lean.Expr.fvar id)
Instances For
Equations
Instances For
Extension storing all function theorems.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Get proof of a theorem.
Equations
Instances For
Structure holding transition or morphism theorems for fun_prop
tactic.
- theorems : Lean.Meta.RefinedDiscrTree GeneralTheorem
Discrimination tree indexing theorems.
Instances For
Extendions for transition or morphism theorems
Equations
Instances For
Environment extension for transition theorems.
Get transition theorems applicable to e
.
For example calling on e
equal to Continuous f
might return theorems implying continuity
from linearity over finite dimensional spaces or differentiability.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Environment extension for morphism theorems.
Get morphism theorems applicable to e
.
For example calling on e
equal to Continuous f
for f : X→L[ℝ] Y
would return theorem
inferring continuity from the bundled morphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
wheref
is a free variable
theorem linear_is_continuous [FiniteDimensional ℝ E] {f : E → F} (hf : IsLinearMap 𝕜 f) :
Continuous f
- lam (thm : LambdaTheorem) : Theorem
- function (thm : FunctionTheorem) : Theorem
- mor (thm : GeneralTheorem) : Theorem
- transition (thm : GeneralTheorem) : Theorem
Instances For
For a theorem declaration declName
return fun_prop
theorem. It correctly detects which
type of theorem it is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Register theorem declName
with fun_prop
.
Equations
- One or more equations did not get rendered due to their size.