bddAbove_Icc

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#bddAbove_Icc

English

The closed interval [a,b] is bounded above by b.

Русский

Замкнутый интервал [a,b] ограничен сверху числом b.

LaTeX

$$$ BddAbove(\ Icc\ a\ b\ ) $$$

Lean4

@[simp]
theorem bddAbove_Icc : BddAbove (Icc a b) :=
  ⟨b, fun _ => And.right⟩

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

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

Разделы

Аффилиация

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