Documentation

Mathlib.Tactic.FunProp.Theorems

fun_prop environment extensions storing theorems for fun_prop #

Stores important argument indices of lambda theorems

For example

theorem Continuous_const {α β} [TopologicalSpace α] [TopologicalSpace β] (y : β) :
    Continuous fun _ : α => y

is represented by

  .const 0 4
Instances For

    There are 5(+1) basic lambda theorems

    • id Continuous fun x => x
    • const Continuous fun x => y
    • proj Continuous fun (f : X → Y) => f x
    • projDep Continuous fun (f : (x : X) → Y x => f x)
    • comp Continuous f → Continuous g → Continuous fun x => f (g x)
    • letE Continuous f → Continuous g → Continuous fun x => let y := g x; f x y
    • pi ∀ y, Continuous (f · y) → Continuous fun x y => f x y
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Instances For
            Equations
            Instances For

              return proof of lambda theorem

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

                    theorem about specific function (either declared constant or free variable)

                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        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
                            Equations

                            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
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For