English
If f and g are functions X → M with HasCompactMulSupport, then their pointwise maximum f ⊔ g also has compact mul support.
Русский
Если функции f и g: X → M имеют компактную опору умножения, то их точечный максимум f ⊔ g тоже имеет компактную опору умножения.
LaTeX
$$$\\forall f,g:\\, X \\to M,\\; HasCompactMulSupport f \\to HasCompactMulSupport g \\to HasCompactMulSupport (f \\uplus g)$$$
Lean4
@[to_additive]
theorem sup {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_sup f g
