inf'_pow — Mathlib

English

The HPow of an inf' over a Finset commutes with taking HPow pointwise inside.

Русский

HPow для inf' над Finset коммутирует с поэлементным HPow внутри.

LaTeX

$$$\text{inf'}\_{{hs}}\, f\^n = \text{inf'}\_{{hs}} \ (\lambda a. f(a)^n)$$$

Lean4

@[to_additive nsmul_inf']
theorem inf'_pow [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs) :
    s.inf' hs f ^ n = s.inf' hs fun a ↦ f a ^ n :=
  map_finset_inf' (OrderHom.mk _ <| pow_left_mono n) hs _

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