Skip to content

Commit

Permalink
Update Mathlib/Topology/ContinuousMap/CompactlySupported.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Yaël Dillies <[email protected]>
  • Loading branch information
yoh-tanimoto and YaelDillies authored Jan 31, 2025
1 parent 4e82463 commit b86d559
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Topology/ContinuousMap/CompactlySupported.lean
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ def ContinuousMap.liftCompactlySupported [CompactSpace α] : C(α, β) ≃ C_c(

/-- Composition of a continuous function `f` with compact support with another continuous function
`g` from the left yields another continuous function `g ∘ f` with compact support. -/
noncomputable def comp_left {γ : Type*} [TopologicalSpace γ] [Zero γ] {g : C(β, γ)}
noncomputable def compLeft {γ : Type*} [TopologicalSpace γ] [Zero γ] (g : C(β, γ))
(f : C_c(α, β)) : C_c(α, γ) where
toContinuousMap := if g 0 = 0 then g.comp f else 0
hasCompactSupport' := by
Expand Down

0 comments on commit b86d559

Please sign in to comment.