isAsymm

Mathlib.Order.WellFounded

URI: https://scilib.ai/kg/mathlib#WellFounded.isAsymm

English

A well-founded relation is asymmetric.

Русский

Хорошо основанное отношение асимметрично.

LaTeX

$$$\text{WellFounded } r \Rightarrow IsAsymm\, α\, r$$$

Lean4

protected theorem isAsymm (h : WellFounded r) : IsAsymm α r :=
  ⟨h.asymmetric⟩

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

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

Разделы

Аффилиация

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