mulSupport_sup — Mathlib

English

For semilatticeSup M, the support of the pointwise supremum of two functions f,g is contained in the union of their supports: mulSupport (f ⊔ g) ⊆ mulSupport f ∪ mulSupport g.

Русский

Для семилатиса Sup множество опор функций: опора функции, равной точечному максимуму f и g, подпадает под объединение опор f и g.

LaTeX

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

Lean4

@[to_additive]
theorem mulSupport_sup [SemilatticeSup M] (f g : α → M) :
    mulSupport (fun x ↦ f x ⊔ g x) ⊆ mulSupport f ∪ mulSupport g :=
  mulSupport_binop_subset (· ⊔ ·) (sup_idem _) f g

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