preimage_relIso — Mathlib

English

If hs is an antichain for r' and φ is a RelIso, then preimage of t is an antichain for r.

Русский

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

LaTeX

$$$IsAntichain(r', t) \rightarrow (\phi : r \cong r') \rightarrow IsAntichain(r, \operatorname{preimage}(\phi, t))$$$

Lean4

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

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