acc_def

Mathlib.Order.WellFounded

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

English

Acc r a is characterized by: for every b with r b a, Acc r b holds.

Русский

Acc r a эквивалентно: для всех b, если r b a, то Acc r b.

LaTeX

$$$Acc\ r\ a \iff \forall b, r b a \to Acc\ r\ b$$$

Lean4

theorem acc_def {α} {r : α → α → Prop} {a : α} : Acc r a ↔ ∀ b, r b a → Acc r b
    where
  mp h := h.rec fun _ h _ ↦ h
  mpr := .intro a

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

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

Разделы

Аффилиация

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