Commit 2022-12-22 13:30 0a5db45f

View on Github →

feat: port Order.Hom.Order (#1152)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Hom/Order.lean

added theorem OrderHom.coe_infᵢ

added theorem OrderHom.coe_supᵢ

added theorem OrderHom.infᵢ_apply

added theorem OrderHom.infₛ_apply

added theorem OrderHom.iterate_sup_le_sup_iff

added theorem OrderHom.supᵢ_apply

added theorem OrderHom.supₛ_apply