Commit 2024-02-14 01:35 73ed7df4

View on Github →

feat(Logic/Function/FromTypes): Add curried heterogeneous function types (#10394) See #10389

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fin/Tuple/Curry.lean

added def Function.FromTypes.curry

added def Function.FromTypes.curryEquiv

added theorem Function.FromTypes.curry_apply_cons

added theorem Function.FromTypes.curry_apply_succ

added theorem Function.FromTypes.curry_two_eq_curry

added theorem Function.FromTypes.curry_uncurry

added def Function.FromTypes.uncurry

added theorem Function.FromTypes.uncurry_apply_cons

added theorem Function.FromTypes.uncurry_apply_succ

added theorem Function.FromTypes.uncurry_curry

added theorem Function.FromTypes.uncurry_two_eq_uncurry

modified def Function.OfArity.curry

modified def Function.OfArity.curryEquiv

added theorem Function.OfArity.curry_two_eq_curry

modified def Function.OfArity.uncurry

added theorem Function.OfArity.uncurry_two_eq_uncurry

Created Mathlib/Logic/Function/FromTypes.lean

added def Function.FromTypes.const

added theorem Function.FromTypes.const_succ

added theorem Function.FromTypes.const_succ_apply

added theorem Function.FromTypes.const_zero

added def Function.FromTypes

added theorem Function.fromTypes_cons

added def Function.fromTypes_cons_equiv

added theorem Function.fromTypes_nil

added def Function.fromTypes_nil_equiv

added theorem Function.fromTypes_succ

added def Function.fromTypes_succ_equiv

added theorem Function.fromTypes_zero

added def Function.fromTypes_zero_equiv

Modified Mathlib/Logic/Function/OfArity.lean

added theorem Function.FromTypes.fromTypes_fin_const

added def Function.FromTypes.fromTypes_fin_const_equiv

modified def Function.OfArity.const

deleted def Function.OfArity

modified theorem Function.ofArity_succ

modified theorem Function.ofArity_zero

Modified Mathlib/SetTheory/ZFC/Basic.lean