le_of_forall_le

Mathlib.Order.Basic

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

English

Let α be a preorder. If every element c with c ≤ a also satisfies c ≤ b, then a ≤ b.

Русский

Пусть α — предупорядоченное множество. Если для каждого элемента c выполняется c ≤ a ⇒ c ≤ b, то a ≤ b.

LaTeX

$$$ (\forall c, c \le a \to c \le b) \to a \le b $$$

Lean4

theorem le_of_forall_le (H : ∀ c, c ≤ a → c ≤ b) : a ≤ b :=
  H _ le_rfl

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

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

Разделы

Аффилиация

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