eq_of_le

Mathlib.Order.Minimal

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

English

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

Русский

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

LaTeX

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

Lean4

theorem eq_of_le (hx : Maximal P x) (hy : P y) (hle : x ≤ y) : x = y :=
  hle.antisymm <| hx.2 hy hle

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

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

Разделы

Аффилиация

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