image_relEmbedding — Mathlib

English

If s is an antichain with respect to r and φ is a relEmbedding r r', then φ''s is an antichain with respect to r'.

Русский

Если s — антицепь относительно r и φ — вложение сопряжённого отношения, то образ φ''s является антицепью относительно r'.

LaTeX

$$$IsAntichain(r,s) \rightarrow (\phi : r \hookrightarrow r') \rightarrow IsAntichain(r', \phi '' s)$$$

Lean4

theorem image_relEmbedding (hs : IsAntichain r s) (φ : r ↪r r') : IsAntichain r' (φ '' s) :=
  by
  intro b hb b' hb' h₁ h₂
  rw [Set.mem_image] at hb hb'
  obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
  exact hs has has' (fun haa' => h₁ (by rw [haa'])) (φ.map_rel_iff.mp h₂)

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