iInf_split_single

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#iInf_split_single

English

The infimum over all i of f i equals f i0 infimum over i ≠ i0, f i (dual form of iSup_split_single).

Русский

Инфинум по всем i равен f(i0) инфиминуму по i ≠ i0 (зеркальная форма).

LaTeX

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

Lean4

theorem iInf_split_single (f : β → α) (i₀ : β) : ⨅ i, f i = f i₀ ⊓ ⨅ (i) (_ : i ≠ i₀), f i :=
  @iSup_split_single αᵒᵈ _ _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru