image_relEmbedding_iff — Mathlib

English

IsAntichain r' (image of s under φ) is equivalent to IsAntichain r s when φ is a RelIso.

Русский

Антицепь r' на образе φ(s) эквивалентна антицепи r на s, когда φ - RelIso.

LaTeX

$$$IsAntichain(r', \operatorname{image}(\phi, s)) \iff IsAntichain(r, s)$$$

Lean4

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

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