image_relEmbedding — Mathlib

English

A detailed statement of image under a RelEmbedding: if φ maps α to β preserving r, then r'-comparability follows in φ''s image.

Русский

Детальное утверждение образа при RelEmbedding: если φ сохраняет порядок, то сопоставимость сохраняется в образе.

LaTeX

$$$\operatorname{IsChain}(r,s) \to \forall a,a' \in s, \; (\text{Or-compatibility of } r' )$$$

Lean4

theorem image_relEmbedding (hs : IsChain r s) (φ : r ↪r r') : IsChain r' (φ '' s) :=
  by
  intro b hb b' hb' h
  rw [Set.mem_image] at hb hb'
  obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
  have := hs has has' (fun haa' => h (by rw [haa']))
  grind [RelEmbedding.map_rel_iff]

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