eq_of_ge

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#Maximal.eq_of_ge

English

If x is Maximal and y satisfies P y with x ≤ y, then y = x.

Русский

Если x максимален и P y выполняется при x ≤ y, то y = x.

LaTeX

$$$ \operatorname{Maximal} P x \to P y \to x \le y \to y = x $$$

Lean4

theorem eq_of_ge (hx : Maximal P x) (hy : P y) (hge : x ≤ y) : y = x :=
  (hx.eq_of_le hy hge).symm

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

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

Разделы

Аффилиация

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