Theorems · Theorem · functional analysis

CompactlySupportedContinuousMap.sup_apply

∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SemilatticeSup β] [inst_2 : Zero β]
  [inst_3 : TopologicalSpace β] [inst_4 : ContinuousSup β] (f g : CompactlySupportedContinuousMap α β) (a : α),
  (f ⊔ g) a = f a ⊔ g a

Defined in

Mathlib.Topology.ContinuousMap.CompactlySupported

Cited by

0 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceSemilatticeSupZeroTopologicalSpaceContinuousSup