instIsIrreflOfIsWellOrder — Mathlib

English

If r is a well-order, then r is irreflexive: for all a, not r a a.

Русский

Если r — хорошо упорядоченное отношение, то оно иррефлексивно: для любого a не выполняется r a a.

LaTeX

$$$(\\mathrm{IsWellOrder}\\ α\\ r) \\rightarrow \\forall a, \\neg r\\ a\\ a$$$

Lean4

instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] : IsIrrefl α r := by
  infer_instance
    -- see Note [lower instance priority]

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