not_prop_of_lt

Mathlib.Order.Minimal

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

English

If x is Minimal for P and y < x, then P y cannot hold.

Русский

Если x минимально по P и y меньше x, то P y не может быть истинно.

LaTeX

$$$ h : \operatorname{Minimal} P x \rightarrow \forall y, y < x \rightarrow \neg P y $$$

Lean4

theorem not_prop_of_lt (h : Minimal P x) (hlt : y < x) : ¬P y :=
  (minimal_iff_forall_lt.1 h).2 hlt

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

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

Разделы

Аффилиация

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