image — Mathlib

English

If s is an antichain with respect to r and f maps α to β with r'-relatedness preserved by f, then f''s is an antichain with respect to r'.

Русский

Если s — антицепь относительно r и f сохраняет взаимноNotRelation, то образ f''s — антицепь относительно r'.

LaTeX

$$$IsAntichain(r,s) \rightarrow (\forall a,b, r'(f a)(f b) \Rightarrow r(a,b)) \Rightarrow IsAntichain(r', f''s)$$$

Lean4

theorem image (hs : IsAntichain r s) (f : α → β) (h : ∀ ⦃a b⦄, r' (f a) (f b) → r a b) : IsAntichain r' (f '' s) :=
  by
  rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ hbc hr
  exact hs hb hc (ne_of_apply_ne _ hbc) (h hr)

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