lift_iSup — Mathlib

English

The lift of a supremum is the supremum of the lifts: lift(iSup f) = ⨆ i, lift(f(i)) (requires bounded above).

Русский

Перенос верхней грани инфимума равен верхней грани перенесённых значений: lift(iSup f) = ⨆ i, lift(f(i)) (при ограниченности сверху).

LaTeX

$$$\text{lift}(\iSup f) = \iSup i\, \text{lift}(f(i))$$$

Lean4

/-- The lift of a supremum is the supremum of the lifts. -/
theorem lift_iSup {ι : Type v} {f : ι → Cardinal.{w}} (hf : BddAbove (range f)) :
    lift.{u} (iSup f) = ⨆ i, lift.{u} (f i) :=
  by
  rw [iSup, iSup, lift_sSup hf, ← range_comp]
  simp [Function.comp_def]

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