lt_blsub_iff — Mathlib

English

For any o and f, a < blsub o f iff there exists i with hi and a ≤ f(i, hi).

Русский

Для любых o и f верно: a < blsub o f эквивалентно существованию i, такого что hi и a ≤ f(i, hi).

LaTeX

$$$\forall o : \mathrm{Ordinal},\ \forall f : (a : \mathrm{Ordinal}) \to a < o \to \mathrm{Ordinal},\ a < \mathrm{blsub}(o,f) \iff \exists i \; hi,\ a \le f(i,hi)$$$

Lean4

theorem lt_blsub_iff {o : Ordinal.{u}} {f : ∀ b < o, Ordinal.{max u v}} {a} :
    a < blsub.{_, v} o f ↔ ∃ i hi, a ≤ f i hi := by
  simpa only [not_forall, not_lt, not_le] using not_congr (@blsub_le_iff.{_, v} _ f a)

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