Theorems · Theorem · general topology

HasCompactSupport.tsupport_extend_zero

∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
  [inst_2 : Zero β] {f : α → β} [T2Space α'],
  HasCompactSupport f →
    ∀ {g : α → α'}, Continuous g → Function.Injective g → tsupport (Function.extend g f 0) = g '' tsupport f

Defined in

Mathlib.Topology.Algebra.Support

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceZeroT2Space