image_iso

Mathlib.Order.Preorder.Chain

URI: https://scilib.ai/kg/mathlib#IsChain.image_iso

English

If s is a chain in α and φ is an order isomorphism from α to β, then φ''s is a chain in β.

Русский

Если s — цепь в α и φ — порядок-изоморфизм α к β, то φ''s — цепь в β.

LaTeX

$$$ IsChain\\ (≤)\\ s \\rightarrow IsChain\\ (≤)\\ (φ '' s) $$$

Lean4

theorem image_iso [LE α] [LE β] (hs : IsChain (· ≤ ·) s) (φ : α ≃o β) : IsChain (· ≤ ·) (φ '' s) :=
  image_relEmbedding hs _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru