enum_zero_le' — Mathlib

English

A variant of the zero bound: for o > 0, a bound holds with a toType embedding.

Русский

Вариант нулевой границы: для o > 0 выполняется ограничение через отображение в toType.

LaTeX

$$$o>0 \\Rightarrow enum_r(⟨0, h0⟩) \\le a$$$

Lean4

theorem enum_zero_le' {o : Ordinal} (h0 : 0 < o) (a : o.toType) :
    enum (α := o.toType) (· < ·) ⟨0, type_toType _ ▸ h0⟩ ≤ a :=
  by
  rw [← not_lt]
  apply enum_zero_le

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