not_prop_of_gt

Mathlib.Order.Minimal

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

English

If x is Maximal for P and hlt: x < y, then ¬P y.

Русский

Если x — максимальное по P, и x < y, то P y невозможно.

LaTeX

$$$ h : \operatorname{Maximal} P x \rightarrow x < y \rightarrow \neg P y $$$

Lean4

theorem not_prop_of_gt (h : Maximal P x) (hlt : x < y) : ¬P y :=
  (maximal_iff_forall_gt.1 h).2 hlt

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

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

Разделы

Аффилиация

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