image_relEmbedding_iff — Mathlib

English

For a RelEmbedding φ from r to r', the chain-ness of the image φ''s is equivalent to the chain-ness of s.

Русский

Для RelEmbedding φ из r в r' цепность образа φ''s эквивалентна цепности s.

LaTeX

$$$ IsChain\ r' (\\phi '' s) \\iff IsChain\\ r s $$$

Lean4

theorem image_relEmbedding_iff {φ : r ↪r r'} : IsChain r' (φ '' s) ↔ IsChain r s :=
  ⟨fun h => (φ.injective.preimage_image s).subst (h.preimage_relEmbedding φ), fun h => h.image_relEmbedding φ⟩

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