image_relIso — Mathlib

English

Let s be a chain with respect to a relation r, and φ be a relational isomorphism from r to r'. Then the image φ''s is a chain with respect to r'.

Русский

Пусть s является цепью относительно отношения r, а φ — отношение-изоморфизм от r к r'. Тогда образ φ''s является цепью относительно r'.

LaTeX

$$$ (IsChain\ r\ s \;\\wedge\\; \\phi : r \\simeq_r r') \\rightarrow IsChain\ r' (\\phi '' s) $$$

Lean4

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

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