exists_eq_iInf

Mathlib.Data.ENat.Lattice

URI: https://scilib.ai/kg/mathlib#ENat.exists_eq_iInf

English

If ι is nonempty, then there exists a such that f(a) = ⨅ x, f x.

Русский

Пусть ι непусто; тогда существует a, такое что f(a) = ⨅ x, f(x).

LaTeX

$$$[Nonempty ι] (f : ι \to \mathbb{N}_\infty) \Rightarrow \exists a, f(a) = \inf_x f(x)$$$

Lean4

theorem exists_eq_iInf [Nonempty ι] (f : ι → ℕ∞) : ∃ a, f a = ⨅ x, f x :=
  csInf_mem (range_nonempty fun i ↦ f i)

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

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

Разделы

Аффилиация

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