inf_apply — Mathlib

English

For f,g in DFinsupp and i in ι, the i-th coordinate of f ⊓ g equals f(i) ⊓ g(i); the infimum is computed coordinatewise.

Русский

Для f,g в DFinsupp и некоторого i из ι, i-я координата (f ⊓ g) равна f(i) ⊓ g(i); инфимум вычисляется координатно.

LaTeX

$$$$ (f \inf g)(i) = f(i) \inf g(i) \quad \text{for all } i. $$$$

Lean4

theorem inf_apply [∀ i, SemilatticeInf (α i)] (f g : Π₀ i, α i) (i : ι) : (f ⊓ g) i = f i ⊓ g i :=
  zipWith_apply _ _ _ _ _

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