Commit 2025-02-03 07:17 d2ce9233

View on Github →

feat(Topology/ContinuousMap/CompactlySupported): add partialOrder (#21206) Add instance : PartialOrder C_c(α, β) using pointwise PartialOrder β, following ContinuousMap.partialOrder

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Order/Support.lean

added theorem HasCompactMulSupport.inf

added theorem HasCompactMulSupport.sup

Modified Mathlib/Topology/ContinuousMap/CompactlySupported.lean

added theorem CompactlySupportedContinuousMap.coe_finsetInf'

added theorem CompactlySupportedContinuousMap.coe_finsetSup'

added theorem CompactlySupportedContinuousMap.coe_inf

added theorem CompactlySupportedContinuousMap.coe_sup

added theorem CompactlySupportedContinuousMap.finsetInf'_apply

added theorem CompactlySupportedContinuousMap.finsetSup'_apply

added theorem CompactlySupportedContinuousMap.inf_apply

added theorem CompactlySupportedContinuousMap.le_def

added theorem CompactlySupportedContinuousMap.lt_def

added theorem CompactlySupportedContinuousMap.sup_apply