Commit 2024-01-09 09:25 043fa2f8

View on Github →

chore(ZeroAtInfty): rename toBcf to toBCF (#9581)

Estimated changes

Modified Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean

added theorem ZeroAtInftyContinuousMap.closed_range_toBCF

deleted theorem ZeroAtInftyContinuousMap.closed_range_toBcf

added theorem ZeroAtInftyContinuousMap.dist_toBCF_eq_dist

deleted theorem ZeroAtInftyContinuousMap.dist_toBcf_eq_dist

added theorem ZeroAtInftyContinuousMap.isometry_toBCF

deleted theorem ZeroAtInftyContinuousMap.isometry_toBcf

added theorem ZeroAtInftyContinuousMap.norm_toBCF_eq_norm

deleted theorem ZeroAtInftyContinuousMap.norm_toBcf_eq_norm

added def ZeroAtInftyContinuousMap.toBCF

added theorem ZeroAtInftyContinuousMap.toBCF_injective

deleted def ZeroAtInftyContinuousMap.toBcf

deleted theorem ZeroAtInftyContinuousMap.toBcf_injective