map_cofinal

Mathlib.Order.Cofinal

URI: https://scilib.ai/kg/mathlib#OrderIso.map_cofinal

English

If e: α ≃o β is an order isomorphism, IsCofinal s → IsCofinal (e '' s).

Русский

Если e: α ≃o β — упорядоченное изоморфизм, то Cofinal s → Cofinal (e''s).

LaTeX

$$IsCofinal s → IsCofinal (e '' s)$$

Lean4

theorem map_cofinal [Preorder β] (e : α ≃o β) {s : Set α} (hs : IsCofinal s) : IsCofinal (e '' s) :=
  e.symm.to_galoisConnection.map_cofinal hs

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

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

Разделы

Аффилиация

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