preimage_relIso — Mathlib

English

If t is a chain with respect to r' and φ is a rel iso from r to r', then the preimage φ⁻¹'(t) is a chain with respect to r.

Русский

Если t является цепью относительно r' и φ — RelIso от r к r', то множество, обратное по φ к t, является цепью относительно r.

LaTeX

$$$ (IsChain\ r'\ t \;\\wedge\\; \\phi : r \\simeq_r r') \\rightarrow IsChain\ r (\\phi^{-1}' t) $$$

Lean4

theorem preimage_relIso {t : Set β} (hs : IsChain r' t) (φ : r ≃r r') : IsChain r (φ ⁻¹' t) :=
  hs.preimage_relEmbedding φ.toRelEmbedding

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