mulSupport_min — Mathlib

English

For linear order M, the support of the pointwise minimum of f and g is contained in the union of their supports: mulSupport (min(f,g)) ⊆ mulSupport f ∪ mulSupport g.

Русский

Для линейного порядка M: опора функции min(f,g) подпадает под объединение опор f и g.

LaTeX

$$$\\text{mulSupport}(\\lambda x. \\min\\{f(x), g(x)\\}) \\subseteq \\text{mulSupport}(f) \\cup \\text{mulSupport}(g).$$$

Lean4

@[to_additive]
theorem mulSupport_min [LinearOrder M] (f g : α → M) :
    mulSupport (fun x ↦ min (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g :=
  mulSupport_inf f g

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