Commit 2024-10-07 11:43 bb5f02d3

feat: fun x ↦ (x ⊓ z, x ⊔ z) is StrictMono in ModularLattice (#17457) In the proof of wellFounded_lt_exact_sequence, it is implicitly shown that fun x : α ↦ (x ⊓ z, x ⊔ z) is StrictMono in a modular lattice, with the lexicographic order on α × α. Here we show the stronger result with α × α equipped with the product order, and golf the proof. If G is not an abelian group, then α = Subgroup G is not necessarily a modular lattice. However, if z is a normal subgroup, the result still holds true. We prove a closely related result strictMono_comap_prod_map which replaces inf with comap and sup with map, so it concerns a function to Subgroup z × Subgroup (G ⧸ z) instead. The same result for submodules immediately implies that Noetherian/Artinian are closed under extensions, which is proven in #17425 using wellFounded_lt/gt_exact_sequence. If z is not even normal, the function to Subgroup z × Set (G ⧸ z) is still StrictMono.