Commit 2022-11-24 08:33 f4bb5531

View on Github →

feat: synchronize with mathlib#16944 (#691) Synchronize with leanprover-community/mathlib#16944

Estimated changes

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.FactorsThrough.apply_extend

added theorem Function.FactorsThrough.extend_apply

added theorem Function.FactorsThrough.extend_comp

added def Function.FactorsThrough

added theorem Function.Injective.FactorsThrough

added theorem Function.Injective.apply_extend

added theorem Function.Injective.extend_apply

deleted theorem Function.apply_extend

deleted theorem Function.extend_apply

added theorem Function.factorsThrough_iff