mulSupport_max — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mulSupport_max [LinearOrder M] (f g : α → M) :
    mulSupport (fun x ↦ max (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g :=
  mulSupport_sup f g

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