ciSup_unique — Mathlib

English

If the index type has a unique element, iSup f equals f at that unique element.

Русский

Если множество индексов имеет единственный элемент, iSup f равен f(уникальному элементу).

LaTeX

$$iSup f = f(default) (when Unique ι)$$

Lean4

@[simp]
theorem ciSup_unique [Unique ι] {s : ι → α} : ⨆ i, s i = s default :=
  by
  have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)
  simp only [this, ciSup_const]

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