Commit 2026-05-05 10:37 26fdeaa7

View on Github →

feat(Order/Directed): directedness under composition by a surjective function (#38861) Also turn directedOn_range around so that the name becomes correct and golf two proofs about directed suprema of subsemigroups/submonoids.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Lattice.lean

Modified Mathlib/Algebra/Group/Submonoid/Membership.lean

modified theorem Submonoid.mem_biSup_of_directedOn

modified theorem Submonoid.mem_iSup_of_directed

Modified Mathlib/Algebra/Group/Subsemigroup/Membership.lean

modified theorem Subsemigroup.mem_biSup_of_directedOn

modified theorem Subsemigroup.mem_iSup_of_directed

Modified Mathlib/CategoryTheory/CofilteredSystem.lean

Modified Mathlib/Data/Fintype/Order.lean

modified theorem Directed.finite_le

added theorem Set.subset_iUnion_iff_of_directed

added theorem Set.subset_sUnion_iff_of_directed

added theorem le_iSup_iff_of_directed

added theorem le_sSup_iff_of_directedOn

Modified Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean

Modified Mathlib/Order/Directed.lean

modified theorem directedOn_range

added theorem directed_comp_iff_of_surjective

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

modified theorem OmegaCompletePartialOrder.Chain.directed