Commit 2024-01-08 12:05 2098be66

View on Github →

refactor: Generalise absolute value of continuous map to topological lattices (#9501) Delete ContinuousMap.abs in favor of the general construction in lattice ordered groups. Part of #9411

Estimated changes

added theorem ContinuousMap.coe_mabs
deleted def ContinuousMap.abs
deleted theorem ContinuousMap.abs_apply
added theorem ContinuousMap.coe_inf'
added theorem ContinuousMap.coe_inf
added theorem ContinuousMap.coe_sup'
added theorem ContinuousMap.coe_sup
modified theorem ContinuousMap.inf'_apply
deleted theorem ContinuousMap.inf'_coe
modified theorem ContinuousMap.inf_apply
deleted theorem ContinuousMap.inf_coe
modified theorem ContinuousMap.sup'_apply
deleted theorem ContinuousMap.sup'_coe
modified theorem ContinuousMap.sup_apply
deleted theorem ContinuousMap.sup_coe