eq_or_eq

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#CovBy.eq_or_eq

English

Let a ⋖ b. If a ≤ c ≤ b, then c is either a or b.

Русский

Пусть a ⋖ b. Если a ≤ c ≤ b, тогда c равно либо a, либо b.

LaTeX

$$(h : a \triangleleft b) (h2 : a \le c) (h3 : c \le b) \Rightarrow c = a \lor c = b$$

Lean4

theorem eq_or_eq (h : a ⋖ b) (h2 : a ≤ c) (h3 : c ≤ b) : c = a ∨ c = b :=
  h.wcovBy.eq_or_eq h2 h3

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

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

Разделы

Аффилиация

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