image_relIso — Mathlib

English

If hs is an antichain for r and φ is a relIso r r', then φ''s is an antichain for r'.

Русский

Если hs — антицепь относительно r и φ — относительное изоморфное вложение, то образ образа является антицепью.

LaTeX

$$$IsAntichain(r,s) \rightarrow (\phi : r \cong r') \rightarrow IsAntichain(r', \phi '' s)$$$

Lean4

theorem image_relIso (hs : IsAntichain r s) (φ : r ≃r r') : IsAntichain r' (φ '' s) :=
  hs.image_relEmbedding φ.toRelEmbedding

Похожие утверждения