mono

Mathlib.Order.Cofinal

URI: https://scilib.ai/kg/mathlib#IsCofinal.mono

English

If s ⊆ t and s is cofinal, then t is cofinal.

Русский

Если s ⊆ t и s софинально, то и t софинально.

LaTeX

$${s t : Set α} (h : s ⊆ t) (hs : IsCofinal s) : IsCofinal t$$

Lean4

theorem mono {s t : Set α} (h : s ⊆ t) (hs : IsCofinal s) : IsCofinal t :=
  by
  intro a
  obtain ⟨b, hb, hb'⟩ := hs a
  exact ⟨b, h hb, hb'⟩

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

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

Разделы

Аффилиация

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