mono_right

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#IsCofinalFor.mono_right

English

If t ⊆ u and s cofinal in t, then s cofinal in u.

Русский

Если t ⊆ u и s кофинально в t, тогда s кофинально в u.

LaTeX

$$$$ t \subseteq u \Rightarrow IsCofinalFor(s,t) \Rightarrow IsCofinalFor(s,u). $$$$

Lean4

protected theorem mono_right (htu : t ⊆ u) (hst : IsCofinalFor s t) : IsCofinalFor s u :=
  hst.trans htu.iscofinalfor

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

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

Разделы

Аффилиация

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