isRelUpperSet_Icc_le

Mathlib.Order.UpperLower.Relative

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

← MathLib Explorer

English

The closed interval [a, c] is an upper set with respect to the relation ≤ c.

Русский

Замкнутый интервал [a, c] является верхним множеством относительно отношения ≤ c.

LaTeX

$$$IsRelUpperSet (Icc a c) (\cdot \le c)$$$

Lean4

theorem isRelUpperSet_Icc_le : IsRelUpperSet (Icc a c) (· ≤ c) := fun _ b ↦
  by
  simp_all only [mem_Icc, and_true, true_and]
  exact fun _ x _ ↦ b.1.trans x

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

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

Разделы

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

Аффилиация

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