Commit 2026-03-11 15:48 e13d3e6e

View on Github →

chore: use RelHomClass in IsChain.image (#34760)

Estimated changes

Modified Counterexamples/AharoniKorman.lean

Modified Mathlib/Order/Height.lean

Modified Mathlib/Order/Preorder/Chain.lean

modified theorem IsChain.image

added theorem IsChain.image_of_map_rel

modified theorem IsChain.image_relEmbedding