iInf_mk — Mathlib

English

The infimum of a pair of indexed sequences equals the pair of infima: ⨅ i, (f i, g i) = (⨅ i, f i, ⨅ i, g i).

Русский

Infimum пары индексированных последовательностей равен паре инфимума соответствующих компонент: ⨅ i, (f i, g i) = (⨅ i, f i, ⨅ i, g i).

LaTeX

$$$\bigl\langle \inf_i f(i), \inf_i g(i) \bigr\rangle = \inf_i (f(i), g(i)).$$$

Lean4

theorem iInf_mk [InfSet α] [InfSet β] (f : ι → α) (g : ι → β) : ⨅ i, (f i, g i) = (⨅ i, f i, ⨅ i, g i) :=
  congr_arg₂ Prod.mk (fst_iInf _) (snd_iInf _)

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