Documentation

Mathlib.Tactic.FunProp.Theorems

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 and gArgId store the argument index for f and g 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

      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.

        Instances For

          Collection of lambda theorems

          Instances For

            Return proof of lambda theorem

            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))
                
                Instances For

                  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

                  • mainArgs : Array

                    array of argument indices about which this theorem is about

                  • appliedArgs :

                    total number of arguments applied to the function

                  • priority :

                    priority

                  • form of the theorem, see documentation of TheoremForm

                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      return proof of function theorem

                      Equations
                      Instances For

                        Extension storing all function theorems.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          General theorem about function property used for transition and morphism theorems

                          Instances For

                            Get proof of a theorem.

                            Equations
                            Instances For

                              Structure holding transition or morphism theorems for fun_prop tactic.

                              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 where f is a free variable
                                      theorem linear_is_continuous [FiniteDimensional ℝ E] {f : E → F} (hf : IsLinearMap 𝕜 f) :
                                          Continuous f
                                    
                                    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.
                                        Instances For