rel_mono

Mathlib.Order.Bounded

URI: https://scilib.ai/kg/mathlib#Set.Unbounded.rel_mono

← MathLib Explorer

English

If r ≤ r' then Bounded r s implies Bounded r' s.

Русский

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

LaTeX

$$rel_mono(h) := Bounded r s → r ≤ r' → Bounded r' s$$

Lean4

theorem rel_mono {r' : α → α → Prop} (hr : r' ≤ r) (h : Unbounded r s) : Unbounded r' s := fun a =>
  let ⟨b, hb, hba⟩ := h a
  ⟨b, hb, fun hba' => hba (hr b a hba')⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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