inf'_eq_csInf_image

Mathlib.Order.ConditionallyCompleteLattice.Finset

URI: https://scilib.ai/kg/mathlib#Finset.inf'_eq_csInf_image

English

For a finite set s and function f, the infimum over s equals the infimum of the image f''s.

Русский

Для конечного множества s и функции f инфimum по s равен инфimumу образа f''s.

LaTeX

$$$\inf_{i∈s} f(i) = \inf (f''s)$$$

Lean4

theorem inf'_eq_csInf_image (s : Finset ι) (H : s.Nonempty) (f : ι → α) : s.inf' H f = sInf (f '' s) :=
  sup'_eq_csSup_image (α := αᵒᵈ) _ H _

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

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

Разделы

Аффилиация

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