preimage_relEmbedding — Mathlib

English

If hs is an antichain for r' and φ is a relEmbedding r r', then IsAntichain r on the preimage of t by φ.

Русский

Если hs — антицепь относительно r' и φ — вложение rel, то предобраз φ⁻¹'(t) является антицепью относительно r.

LaTeX

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

Lean4

theorem preimage_relEmbedding {t : Set β} (ht : IsAntichain r' t) (φ : r ↪r r') : IsAntichain r (φ ⁻¹' t) :=
  fun _ ha _s ha' hne hle => ht ha ha' (fun h => hne (φ.injective h)) (φ.map_rel_iff.mpr hle)

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