image_relIso_iff

Mathlib.Order.Preorder.Chain

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

English

Let φ be a relIso from r to r'. Then IsChain r' (φ''s) holds if and only if IsChain r s holds.

Русский

Пусть φ — RelIso от r к r'. Тогда IsChain r'(φ''s) эквивалентно IsChain r(s).

LaTeX

$$$ IsChain\\ r' (φ '' s) \\iff IsChain\\ r s $$$

Lean4

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

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

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

Разделы

Аффилиация

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