eq_of_ge

Mathlib.Order.Minimal

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

English

If x is Minimal with respect to P and y satisfies P y and y ≤ x, then x = y.

Русский

Если x минимально по P и P y и y ≤ x, то x = y.

LaTeX

$$$ \text{Minimal } P x \to P y \to y \le x \to x = y $$$

Lean4

theorem eq_of_ge (hx : Minimal P x) (hy : P y) (hge : y ≤ x) : x = y :=
  (hx.2 hy hge).antisymm hge

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

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

Разделы

Аффилиация

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