iInf_ulift — Mathlib

English

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

Русский

Для любой f: ULift ι → α справедливо: inf_{i: ULift ι} f(i) = inf_{i: ι} f(up(i)).

LaTeX

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

Lean4

@[simp]
theorem iInf_ulift {ι : Type*} [InfSet α] (f : ULift ι → α) : ⨅ i : ULift ι, f i = ⨅ i, f (.up i) := by
  simp only [iInf]; congr with x; simp

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