notMem_uIcc_of_gt

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.notMem_uIcc_of_gt

English

If a < c and b < c, then c is not in [[a,b]].

Русский

Если a < c и b < c, то c не принадлежит [[a,b]].

LaTeX

$$$(a < c) \land (b < c) \Rightarrow c \notin [[a, b]]$$$

Lean4

theorem notMem_uIcc_of_gt : a < c → b < c → c ∉ [[a, b]] :=
  by
  rw [mem_uIcc]
  exact Set.notMem_uIcc_of_gt

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

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

Разделы

Аффилиация

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