English
If f is injective and h relates s on β to r on α, then the preimage of a chain under f is a chain on α.
Русский
Если f инъективно, и h связывает s на β с r на α, тогда обратное изображение цепи по f является цепью на α.
LaTeX
$$$\operatorname{IsChain}(r, f^{-1}[c])$ given injective f and $\forall x,y\, s(fx,fy) \to r x y$ and $\operatorname{IsChain}(s,c)$$$
Lean4
theorem image (r : α → α → Prop) (s : β → β → Prop) (f : α → β) (h : ∀ x y, r x y → s (f x) (f y)) {c : Set α}
(hrc : IsChain r c) : IsChain s (f '' c) := fun _ ⟨_, ha₁, ha₂⟩ _ ⟨_, hb₁, hb₂⟩ =>
ha₂ ▸ hb₂ ▸ fun hxy => (hrc ha₁ hb₁ <| ne_of_apply_ne f hxy).imp (h _ _) (h _ _)
