iSup_unique — Mathlib

English

If ι has a unique element, the supremum of f over ι equals f of that unique element: ⨆ i, f(i) = f(default) where default is the unique element.

Русский

Если у ι имеется единственный элемент, то ⨆ i, f(i) = f(единственный элемент).

LaTeX

$$$\\\\iSup i, f(i) = f\\\$default\\\$$$$

Lean4

theorem iSup_unique [Unique ι] (f : ι → α) : ⨆ i, f i = f default := by
  simp only [congr_arg f (Unique.eq_default _), iSup_const]

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