mono

Mathlib.Order.Bounded

URI: https://scilib.ai/kg/mathlib#Set.Bounded.mono

English

If s ⊆ t and t is r-bounded, then s is r-bounded.

Русский

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

LaTeX

$$$s\subseteq t \quad\to\quad Bounded\,r\,t \;\to\; Bounded\,r\,s$$$

Lean4

theorem mono (hst : s ⊆ t) (hs : Bounded r t) : Bounded r s :=
  hs.imp fun _ ha b hb => ha b (hst hb)

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

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

Разделы

Аффилиация

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