iInf_split — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iInf_split : ∀ (f : β → α) (p : β → Prop), ⨅ i, f i = (⨅ (i) (_ : p i), f i) ⊓ ⨅ (i) (_ : ¬p i), f i :=
  @iSup_split αᵒᵈ _ _

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