Commit 2023-06-08 04:21 76deb42c

View on Github →

feat: port Topology.ContinuousFunction.Units (#4818)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/Units.lean

added theorem ContinuousMap.continuous_isUnit_unit

added theorem ContinuousMap.isUnit_iff_forall_isUnit

added theorem ContinuousMap.isUnit_iff_forall_ne_zero

added theorem ContinuousMap.spectrum_eq_range

added def ContinuousMap.unitsLift

added theorem ContinuousMap.unitsLift_apply_inv_apply

added theorem ContinuousMap.unitsLift_symm_apply_apply_inv'