Theorems · Theorem · general topology

tsupport_smul_subset_left

∀ {X : Type u_1} [inst : TopologicalSpace X] {M : Type u_9} {α : Type u_10} [inst_1 : Zero M] [inst_2 : Zero α]
  [inst_3 : SMulWithZero M α] (f : X → M) (g : X → α), (tsupport fun x => f x • g x) ⊆ tsupport f

Defined in

Mathlib.Topology.Algebra.Support

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceZeroZeroSMulWithZero