rank_range — Mathlib

English

For a small index type α and f: α → ZFSet, the rank of range f is the supremum of succ(rank(f i)) over i.

Русский

Для малого множества индексов α и отображения f: α → ZFSet, ранг диапазона range f равен наибольшему верхнему пределу succ(rank(f i)) по i.

LaTeX

$$$$ \operatorname{rank}(\operatorname{range} f) = \bigvee_{i} \operatorname{succ}( \operatorname{rank}(f i) ) $$$$

Lean4

@[simp]
theorem rank_range {α : Type*} [Small.{u} α] (f : α → ZFSet.{u}) : rank (range f) = ⨆ i, succ (rank (f i)) :=
  by
  apply (Ordinal.iSup_le _).antisymm'
  · simpa [rank_le_iff, ← succ_le_iff] using Ordinal.le_iSup _
  · simp [rank_lt_of_mem]

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