image_relIso_iff — Mathlib

English

Equivalence between IsAntichain r' on image under RelIso and IsAntichain r on original set.

Русский

Эквивалентность антицепи между образами относительно RelIso и исходным множеством.

LaTeX

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

Lean4

theorem image_relIso_iff {φ : r ≃r r'} : IsAntichain r' (φ '' s) ↔ IsAntichain r s :=
  @image_relEmbedding_iff _ _ _ _ _ (φ : r ↪r r')

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