blsub_le_iff — Mathlib

English

A is less than blsub o f if and only if there exists i, hi with a ≤ f i hi.

Русский

Пусть a < b; тогда a < blsub o f тогда и только тогда, когда существует i, hi, such that a ≤ f i hi.

LaTeX

$$$a < blsub f \;\Leftrightarrow\; \exists i, hi, a \le f i hi$$$

Lean4

theorem blsub_le_iff {o : Ordinal.{u}} {f : ∀ a < o, Ordinal.{max u v}} {a} : blsub.{_, v} o f ≤ a ↔ ∀ i h, f i h < a :=
  by
  convert bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a) using 2
  simp_rw [succ_le_iff]

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