iSup_ulift — Mathlib

English

For any f: ULift ι → α, the supremum over ULift-indexed arguments equals the supremum over the underlying index with the up-map: sup_{i: ULift ι} f(i) = sup_{i: ι} f(up(i)).

Русский

Для любой f: ULift ι → α выполняется равенство: sup_{i: ULift ι} f(i) = sup_{i: ι} f(up(i)).

LaTeX

$$$$ \sup_{i : \mathrm{ULift}\, \i} f(i) = \sup_{i : \i} f(\mathrm{up}(i)) $$$$

Lean4

@[simp]
theorem iSup_ulift {ι : Type*} [SupSet α] (f : ULift ι → α) : ⨆ i : ULift ι, f i = ⨆ i, f (.up i) := by
  simp only [iSup]; congr with x; simp

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