The topological support of sup and inf of functions

In a topological space X and a space M with Sup structure, for f g : X → M with compact support, we show that f ⊔ g has compact support. Similarly, in β with Inf structure, f ⊓ g has compact support if so do f and g.

theorem HasCompactMulSupport.sup {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [One M] [SemilatticeSup M] {f g : X → M} (hf : HasCompactMulSupport f) (hg : HasCompactMulSupport g) : HasCompactMulSupport (f ⊔ g)

theorem HasCompactSupport.sup {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [Zero M] [SemilatticeSup M] {f g : X → M} (hf : HasCompactSupport f) (hg : HasCompactSupport g) : HasCompactSupport (f ⊔ g)

theorem HasCompactMulSupport.inf {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [One M] [SemilatticeInf M] {f g : X → M} (hf : HasCompactMulSupport f) (hg : HasCompactMulSupport g) : HasCompactMulSupport (f ⊓ g)

theorem HasCompactSupport.inf {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [Zero M] [SemilatticeInf M] {f g : X → M} (hf : HasCompactSupport f) (hg : HasCompactSupport g) : HasCompactSupport (f ⊓ g)