English
A detailed statement of image under a RelEmbedding: if φ maps α to β preserving r, then r'-comparability follows in φ''s image.
Русский
Детальное утверждение образа при RelEmbedding: если φ сохраняет порядок, то сопоставимость сохраняется в образе.
LaTeX
$$$\operatorname{IsChain}(r,s) \to \forall a,a' \in s, \; (\text{Or-compatibility of } r' )$$$
Lean4
theorem image_relEmbedding (hs : IsChain r s) (φ : r ↪r r') : IsChain r' (φ '' s) :=
by
intro b hb b' hb' h
rw [Set.mem_image] at hb hb'
obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
have := hs has has' (fun haa' => h (by rw [haa']))
grind [RelEmbedding.map_rel_iff]