lt — Mathlib · SciLib

English

If h is a fundamental sequence, then s p hp < a for p below o according to the lt relation.

Русский

Если h — фундаментальная последовательность, то для любой p < o выполняется s p hp < a по отношению к порядку lt.

LaTeX

$$$$\forall p

Lean4

protected theorem lt {a o : Ordinal} {s : Π p < o, Ordinal} (h : IsFundamentalSequence a o s) {p : Ordinal}
    (hp : p < o) : s p hp < a :=
  h.blsub_eq ▸ lt_blsub s p hp

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