eq_or_eq

Mathlib.Order.Cover

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

← MathLib Explorer

English

If a ⩿ b and a ≤ c ≤ b, then c equals a or c equals b.

Русский

Если a ⩿ b и a ≤ c ≤ b, то c равно a или c равно b.

LaTeX

$$$$\forall {a,b,c}:\alpha,\; a⩿b\to a\le c\to c\le b\to c=a\lor c=b.$$$$

Lean4

theorem eq_or_eq (h : a ⩿ b) (h2 : a ≤ c) (h3 : c ≤ b) : c = a ∨ c = b :=
  by
  rcases h2.eq_or_lt with (h2 | h2); · exact Or.inl h2.symm
  rcases h3.eq_or_lt with (h3 | h3); · exact Or.inr h3
  exact (h.2 h2 h3).elim

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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