min_lt_of_right_lt

Mathlib.Order.MinMax

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

English

Let α be a linearly ordered set. For all a, b, c ∈ α, if b < c then min(a, b) < c.

Русский

Пусть α — линейно упорядоченное множество. Для любых a, b, c ∈ α верно: b < c ⇒ min(a, b) < c.

LaTeX

$$$$\forall a,b,c \in \alpha,\ b < c \Rightarrow \min(a,b) < c.$$$$

Lean4

theorem min_lt_of_right_lt (h : b < c) : min a b < c :=
  (min_le_right a b).trans_lt h

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

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

Разделы

Аффилиация

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