Theorems · Theorem · general topology

HasCompactSupport.comp_isClosedEmbedding

∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
  [inst_2 : Zero β] {f : α → β},
  HasCompactSupport f → ∀ {g : α' → α}, Topology.IsClosedEmbedding g → HasCompactSupport (f ∘ g)

Defined in: Mathlib.Topology.Algebra.Support
Cited by: 3 results in Mathlib
Foundations: Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace Zero

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites19

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

Setproof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Set.preimageproof · cited by 4,946
IsCompactproof · cited by 1,282
closureproof · cited by 1,254
Function.supportproof · cited by 610
HasCompactSupportstatement and proof · cited by 196
Topology.IsClosedEmbeddingstatement and proof · cited by 195
isClosed_closureproof · cited by 195
tsupportproof · cited by 178
closure_monoproof · cited by 133
Set.preimage_monoproof · cited by 95

Cited by3

Results whose statement or proof uses this declaration.

HasCompactSupport.comp_homeomorphproof · cited by 10
MeasureTheory.Measure.addHaarScalarFactor_domSMulproof · cited by 3
MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_auxproof · cited by 1