ciInf_eq_ite — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem ciInf_eq_ite {p : Prop} [Decidable p] {f : p → α} : (⨅ h : p, f h) = if h : p then f h else sInf (∅ : Set α) :=
  ciSup_eq_ite (α := αᵒᵈ)

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