Theorems · Theorem · general topology

HasCompactSupport.comp_smul

∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {β : Type u_5} [inst_4 : Zero β] {f : α → β},
  HasCompactSupport f → ∀ {c : G₀}, c ≠ 0 → HasCompactSupport fun x => f (c • x)

Defined in: Mathlib.Topology.Algebra.ConstMulAction
Cited by: 0 results in Mathlib
Foundations: Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace GroupWithZero MulAction ContinuousConstSMul Zero

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
MulActionstatement and proof · cited by 1,294
ContinuousConstSMulstatement and proof · cited by 832
GroupWithZerostatement and proof · cited by 691
HasCompactSupportstatement and proof · cited by 196
Homeomorph.smulOfNeZeroproof · cited by 11
HasCompactSupport.comp_homeomorphproof · cited by 10

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.