Commit 2024-07-14 20:25 779a1e4b

View on Github →

feat: Monotonicity of monadic operations on Part (#13337) Prove that Part.bind, Part.map and seq respect monotonicity of functions. Rename OrderHom.bind to OrderHom.partBind.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Monotone/Basic.lean

added theorem antitone_iff_apply₂

added theorem monotone_iff_apply₂

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

deleted def OrderHom.bind

Created Mathlib/Order/Part.lean

added theorem Antitone.partBind

added theorem Antitone.partMap

added theorem Antitone.partSeq

added theorem Monotone.partBind

added theorem Monotone.partMap

added theorem Monotone.partSeq

added def OrderHom.partBind