coe_inf

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.coe_inf

English

The underlying function of f ⊓ g equals the pointwise min of f and g.

Русский

Соответствующая функция для f ⊓ g равна точечному минимуму.

LaTeX

$$$\uparrow(f \land g)(n)=\min\{f(n),g(n)\}\quad(\forall n).$$$

Lean4

@[simp, norm_cast]
theorem coe_inf (f g : CauSeq α abs) : ⇑(f ⊓ g) = (f : ℕ → α) ⊓ g :=
  rfl

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

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

Разделы

Аффилиация

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