inf — Mathlib

English

If f and g are quasiconcave on S, then their pointwise infimum k = f ⊓ g is quasiconcave on S.

Русский

Если f и g на S квазиконкавны, то их точечный инфимум k = f ⊓ g также квазиконкавен на S.

LaTeX

$$$QuasiconcaveOn\ 𝕜\ s\ f \rightarrow QuasiconcaveOn\ 𝕜\ s\ g \rightarrow QuasiconcaveOn\ 𝕜\ s\ (f \⊓\ g)$$$

Lean4

theorem inf [SemilatticeInf β] (hf : QuasiconcaveOn 𝕜 s f) (hg : QuasiconcaveOn 𝕜 s g) : QuasiconcaveOn 𝕜 s (f ⊓ g) :=
  hf.dual.sup hg

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