Strict-monotone preimage of an antichain

[UPSTREAM] candidate for Mathlib/Order/Antichain.lean: a StrictMono pullback lemma for ≤-antichains, complementing mathlib's existing IsAntichain.preimage (injective + relation-preserving) and IsAntichain.preimage_embedding (order embeddings). On a partial order StrictMono is strictly weaker than Injective ∧ Monotone, so this generalizes the ≤-instance of preimage.

This file mirrors mathlib's Order/Antichain.lean path: on upstreaming, the lemma moves verbatim into namespace IsAntichain there and this file is deleted.

Main statements

• IsAntichain.preimage_strictMono

theorem IsAntichain.preimage_strictMono {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {s : Set β} (hs : IsAntichain (fun (x1 x2 : β) => x1 ≤ x2) s) {f : α → β} (hf : StrictMono f) : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) (f ⁻¹' s)

The preimage of a ≤-antichain under a strictly monotone map is a ≤-antichain. Unlike IsAntichain.preimage (which needs f injective and relation-preserving) and IsAntichain.preimage_embedding (order embeddings), this needs only StrictMono f — strictly weaker on a partial order.