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)