bsup'_eq_iSup — Mathlib

English

The simp lemma bsup'_eq_iSup expresses bsup as iSup in a canonical form.

Русский

Симп-лемма bsup'_eq_iSup выражает bsup как iSup в канонической форме.

LaTeX

$$$$ bsup'(r,f) = \\mathrm{iSup} (bfamilyOfFamily' r f) $$$$

Lean4

@[simp]
theorem bsup'_eq_iSup {ι} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal) :
    bsup _ (bfamilyOfFamily' r f) = iSup f := by
  simp +unfoldPartialApp only [← iSup'_eq_bsup r, enum_typein, familyOfBFamily', bfamilyOfFamily']

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