Results for mathlib

A collection of results for the disproof of the Aharoni–Korman conjecture which should be in mathlib.

theorem LeanPool.AharoniKorman.chain_intersect_antichain {α : Type u_1} [PartialOrder α] {s t : Set α} (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) (ht : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) t) : (s ∩ t).Subsingleton