ciSup_eq_ite — Mathlib

English

For a decidable proposition p, the indexed supremum over p of f equals f on p if p holds, else the supremum over the empty set.

Русский

Для разрешимого по p предложения p вершина iSup по p равна f(h) при p, иначе равна sSup(∅).

LaTeX

$$iSup_{h : p} f(h) = if h : p then f(h) else sSup(∅ : Set α)$$

Lean4

theorem ciSup_eq_ite {p : Prop} [Decidable p] {f : p → α} : (⨆ h : p, f h) = if h : p then f h else sSup (∅ : Set α) :=
  by by_cases H : p <;> simp [ciSup_neg, H]

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