iSup_split — Mathlib

English

For any f: β → α and i0 ∈ β, the infimum over all i of f(i) equals the infimum of f(i0) and the infimum over all i ≠ i0 of f(i).

Русский

Для любой функции f: β → α и фиксированного i0 ∈ β инфиминум по всем i равен инфиминуму f(i0) и инфиминуму по всем i ≠ i0.

LaTeX

$$$$ \\inf_i f(i) = \\inf\\{ f(i_0) , \\inf_{i \\neq i_0} f(i) \\} $$$$

Lean4

theorem iSup_split (f : β → α) (p : β → Prop) : ⨆ i, f i = (⨆ (i) (_ : p i), f i) ⊔ ⨆ (i) (_ : ¬p i), f i := by
  simpa [Classical.em] using @iSup_union _ _ _ f {i | p i} {i | ¬p i}

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