Commit 2026-09-13 23:47 2ff8073d

feat: Std.Total instance for InvImage (#43326) This PR fills in the transfer of unbundled relation classes along InvImage and Order.Preimage, so that both spellings carry everything Function.onFun already has. InvImage gains Std.Refl, Std.Symm, Std.Asymm, Std.Total, IsPreorder, IsEquiv, IsStrictOrder and IsStrictWeakOrder instances, along with antisymm, trichotomous, isPartialOrder, isLinearOrder and isStrictTotalOrder for injective f. (Std.Irrefl and IsTrans are already in Mathlib/Order/Defs/Unbundled.lean.) These are stated for Sort, matching core's InvImage. Order.Preimage gains the four injectivity lemmas trichotomous, isPartialOrder, isLinearOrder and isStrictTotalOrder. All of these are definitionally the Function.onFun versions, and are proved by inferInstanceAs, but instance search does not fire on goals stated with InvImage or ⁻¹'o (and InvImage is how goals arise from WellFoundedRelation-adjacent and Sum.Lex-based constructions). Used in https://github.com/leanprover/cslib/pull/401.

example {α β : Type} (r : α → α → Prop) [Std.Total r] (f : β → α) :
    Std.Total (InvImage r f) := inferInstance

🤖 Prepared with Claude Code