Commit 2024-09-10 10:43 18adea12

View on Github →

feat(Topology/ContinuousFunction/Bounded): add the ideal of compactly supported functions (#12629) add the ideal of compactly supported function and introduce the notations. Motivation: the space of compactly supported functions may have different topologies. For the uniform norm, it was suggested to define it as a subtype of α →ᵇ γ on Zulip Maybe I should add a similar subtype to ZeroAtInfty.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean

added theorem TwoSidedIdeal.mem_top

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

Created Mathlib/Topology/ContinuousFunction/BoundedCompactlySupported.lean

added def compactlySupported

added theorem compactlySupported_eq_top

added theorem compactlySupported_eq_top_iff

added theorem compactlySupported_eq_top_of_isCompact

added theorem exist_norm_eq

added theorem mem_compactlySupported

added theorem norm_lt_iff_of_compactlySupported

added theorem norm_lt_iff_of_nonempty_compactlySupported

added def ofCompactSupport

added theorem ofCompactSupport_mem

Modified Mathlib/Topology/Support.lean