exists_not_acc_lt_of_not_acc

Mathlib.Order.WellFounded

URI: https://scilib.ai/kg/mathlib#exists_not_acc_lt_of_not_acc

← MathLib Explorer

English

If a is not Acc r, then there exists b with not Acc r b and r b a.

Русский

Если a не Acc r, существует b such that не Acc r b и r b a.

LaTeX

$$$(\neg Acc\ r\ a) \Rightarrow \exists b, (\neg Acc\ r\ b) \land r b a$$$

Lean4

theorem exists_not_acc_lt_of_not_acc {α} {a : α} {r} (h : ¬Acc r a) : ∃ b, ¬Acc r b ∧ r b a :=
  by
  rw [acc_def] at h
  push_neg at h
  simpa only [and_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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