Commit 2023-03-02 09:07 29664000

View on Github →

feat: port Control.LawfulFix (#1739)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/LawfulFix.lean

added theorem LawfulFix.fix_eq'

added def Part.Fix.approxChain

added theorem Part.Fix.approx_le_fix

added theorem Part.Fix.approx_mem_approxChain

added theorem Part.Fix.approx_mono'

added theorem Part.Fix.approx_mono

added theorem Part.Fix.exists_fix_le_approx

added theorem Part.Fix.le_f_of_mem_approx

added theorem Part.Fix.mem_iff

added theorem Part.fix_eq

added theorem Part.fix_eq_ωSup

added theorem Part.fix_le

added def Part.toUnitMono

added theorem Part.to_unit_cont

added theorem Pi.continuous_curry

added theorem Pi.continuous_uncurry

added def Pi.monotoneCurry

added def Pi.monotoneUncurry

added theorem Pi.uncurry_curry_continuous