English
If hs is a strong antichain on s and f is injective with order-reflecting compatibility, then the preimage f^{-1}(s) is a strong antichain.
Русский
Если s является сильной антицепью и f инъективна с сохранением порядка в обратном отношении, то предобраз f^{-1}(s) является сильной антицепью.
LaTeX
$$$\\text{IsStrongAntichain}(r, s) \\Rightarrow \\forall f:\\beta\\to\\alpha,\\ \\text{Injective}(f) \\land (\\forall a,b, r'(a,b) \\Rightarrow r(f a)(f b)) \\Rightarrow \\text{IsStrongAntichain}(r', f^{-1}(s))$$$
Lean4
theorem preimage (hs : IsStrongAntichain r s) {f : β → α} (hf : Injective f) (h : ∀ a b, r' a b → r (f a) (f b)) :
IsStrongAntichain r' (f ⁻¹' s) := fun _ ha _ hb hab _ => (hs ha hb (hf.ne hab) _).imp (mt <| h _ _) (mt <| h _ _)
