mulSupport_inf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mulSupport_inf [SemilatticeInf M] (f g : α → M) :
    mulSupport (fun x ↦ f x ⊓ g x) ⊆ mulSupport f ∪ mulSupport g :=
  mulSupport_binop_subset (· ⊓ ·) (inf_idem _) f g

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