English
If hs is an antichain with respect to r and f is injective with r'-relation preserved by f, then the preimage f^{-1}(s) is an antichain with respect to r'.
Русский
Если hs — антицепь относительно r и f — инъекция, сохраняющая отношения, то предобраз f^{-1}(s) — антицепь относительно r'.
LaTeX
$$$IsAntichain(r,s) \rightarrow (Injective f) \rightarrow (\forall a,b, r'(a,b) \Rightarrow r(f a, f b)) \Rightarrow IsAntichain(r', f^{-1}(s))$$$
Lean4
theorem preimage (hs : IsAntichain r s) {f : β → α} (hf : Injective f) (h : ∀ ⦃a b⦄, r' a b → r (f a) (f b)) :
IsAntichain r' (f ⁻¹' s) := fun _ hb _ hc hbc hr => hs hb hc (hf.ne hbc) <| h hr
