isRelLowerSet_Icc_ge

Mathlib.Order.UpperLower.Relative

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

English

The interval [c, a] is a RelLowerSet with respect to the predicate c ≤ ·.

Русский

Интервал [c, a] является RelLowerSet относительно предиката c ≤ ·.

LaTeX

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

Lean4

theorem isRelLowerSet_Icc_ge : IsRelLowerSet (Icc c a) (c ≤ ·) := fun _ b ↦
  by
  simp_all only [mem_Icc, true_and]
  exact fun _ x _ ↦ x.trans b.2

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

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

Разделы

Аффилиация

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