irrefl — Mathlib

English

There is no f : r ≺i r when IsWellOrder α r; equivalently, the type PrincipalSeg r r is empty.

Русский

Не существует отображения f : r ≺i r при условии, что α упорядочено хорошо по r; эквивалентно тому, что множество PrincipalSeg r r пусто.

LaTeX

$$$\neg \exists f : r \prec i r$$$

Lean4

theorem irrefl {r : α → α → Prop} [IsWellOrder α r] (f : r ≺i r) : False :=
  by
  have h := f.lt_top f.top
  rw [show f f.top = f.top from InitialSeg.eq f (InitialSeg.refl r) f.top] at h
  exact _root_.irrefl _ h

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