English
If f and g are functions with HasCompactMulSupport, then their pointwise minimum f ⊓ g also has compact mul support.
Русский
Если функции f и g обладают компактной опорой умножения, то их точечное минимальное значение f ⊓ g тоже имеет компактную опору умножения.
LaTeX
$$$\\forall f,g:\\, X \\to M,\\; HasCompactMulSupport f \\to HasCompactMulSupport g \\to HasCompactMulSupport (f \\sqcap g)$$$
Lean4
@[to_additive]
theorem inf {f g : X → M} (hf : HasCompactMulSupport f) (hg : HasCompactMulSupport g) : HasCompactMulSupport (f ⊓ g) :=
by
apply IsCompact.of_isClosed_subset (IsCompact.union hf hg) (isClosed_mulTSupport _)
rw [mulTSupport, mulTSupport, mulTSupport, ← closure_union]
apply closure_mono
exact Function.mulSupport_inf f g
