preimage_relEmbedding — Mathlib

English

If ht: IsChain r' t and φ: r ↪r r' is a RelEmbedding, then the preimage under φ is a chain in r.

Русский

Если ht: IsChain r' t и φ: r ↪r r' — RelEmbedding, то предобраз по φ образует цепь в r.

LaTeX

$$$\operatorname{IsChain}(r, \mathrm{preimage}\, \phi\, t)$$$

Lean4

theorem preimage_relEmbedding {t : Set β} (ht : IsChain r' t) (φ : r ↪r r') : IsChain r (φ ⁻¹' t) :=
  fun _ ha _s ha' hne => by
  have := ht ha ha' (fun h => hne (φ.injective h))
  grind [RelEmbedding.map_rel_iff]

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