English
If hs is a strong antichain on s and f is surjective with order-preserving compatibility, then the image f''s is a strong antichain.
Русский
Если s является сильной антицепью по r и образ f(s) существующей функции сохраняет порядок, то образ f''s является сильной антицепью.
LaTeX
$$$\\text{IsStrongAntichain}(r, s) \\Rightarrow \\forall f,\\ \\text{Surjective}(f) \\land (\\forall a,b, r'(f a)(f b) \\\\Rightarrow r a b) \\Rightarrow \\text{IsStrongAntichain}(r', \\{f(a) \\mid a \\in s\\})$$$
Lean4
theorem image (hs : IsStrongAntichain r s) {f : α → β} (hf : Surjective f) (h : ∀ a b, r' (f a) (f b) → r a b) :
IsStrongAntichain r' (f '' s) := by
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c
obtain ⟨c, rfl⟩ := hf c
exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)
