Injectivity of CompleteLatticeHom.setPreimage

Mathlib.Order.Hom.CompleteLattice packages set-preimage f⁻¹ of a function f : Y → X as a CompleteLatticeHom (Set X) (Set Y) via CompleteLatticeHom.setPreimage. This file establishes that the packaging is injective in f: distinct functions induce distinct set-preimage operators.

The proof probes the operator at the singleton {f y} to extract g y = f y pointwise — the same atom-decomposition technique that underlies @cite{hoeksema-1983} Fact 1 (uniqueness of NP-comparative GQ homomorphisms from their threshold functions).

Candidate for upstreaming to mathlib.

theorem Core.Order.setPreimage_injective {X : Type u_1} {Y : Type u_2} : Function.Injective CompleteLatticeHom.setPreimage

CompleteLatticeHom.setPreimage is injective in its function argument.