isIrrefl

Mathlib.Order.Defs.Unbundled

URI: https://scilib.ai/kg/mathlib#IsAsymm.isIrrefl

English

If r is asymmetric, then r is irreflexive.

Русский

Если r асимметрично, то r иррефлексивно.

LaTeX

$$$\\\\forall r \\\\ [IsAsymm \\\\alpha \\\\ r], \\\\ IsIrrefl \\\\alpha \\\\ r.$$$

Lean4

protected theorem isIrrefl [IsAsymm α r] : IsIrrefl α r :=
  ⟨fun _ h => _root_.asymm h h⟩

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

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

Разделы

Аффилиация

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