enum_zero_le — Mathlib

English

If type r is nonzero, then zero is the least element of the type α under r, and no a is below enum r ⟨0,h0⟩.

Русский

Если тип r не нулевой, то ниже по порядку нулевой элемент в α и не существует элемента меньше enum r ⟨0,h0⟩.

LaTeX

$$$0 < type(r) \\implies \\forall a, \\lnot r(a, enum_r(⟨0,h\\rangle))$$$

Lean4

theorem enum_zero_le {r : α → α → Prop} [IsWellOrder α r] (h0 : 0 < type r) (a : α) : ¬r a (enum r ⟨0, h0⟩) :=
  by
  rw [← enum_typein r a, enum_le_enum r]
  apply Ordinal.zero_le

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