unbounded_lt_of_unbounded_le

Mathlib.Order.Bounded

URI: https://scilib.ai/kg/mathlib#Set.unbounded_lt_of_unbounded_le

English

If r' ≤ r and s is Unbounded r s, then s is Unbounded r' s.

Русский

Если r' ≤ r и s неограничено по r, то неограничено по r'.

LaTeX

$$rel_mono(hr : r' ≤ r) (h : Unbounded r s) : Unbounded r' s$$

Lean4

theorem unbounded_lt_of_unbounded_le [Preorder α] (h : Unbounded (· ≤ ·) s) : Unbounded (· < ·) s :=
  h.rel_mono fun _ _ => le_of_lt

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

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

Разделы

Аффилиация

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