Commit 2023-05-08 21:09 c4182441

View on Github →

feat: port Topology.ContinuousFunction.Algebra (#3332)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/Algebra.lean

added def ContinuousMap.C

added theorem ContinuousMap.C_apply

added def ContinuousMap.coeFnAlgHom

added def ContinuousMap.coeFnLinearMap

added def ContinuousMap.coeFnMonoidHom

added def ContinuousMap.coeFnRingHom

added theorem ContinuousMap.coe_div

added theorem ContinuousMap.coe_int_cast

added theorem ContinuousMap.coe_inv

added theorem ContinuousMap.coe_mul

added theorem ContinuousMap.coe_nat_cast

added theorem ContinuousMap.coe_one

added theorem ContinuousMap.coe_pow

added theorem ContinuousMap.coe_prod

added theorem ContinuousMap.coe_smul

added theorem ContinuousMap.coe_star

added theorem ContinuousMap.coe_zpow

added def ContinuousMap.compMonoidHom'

added def ContinuousMap.compRightAlgHom

added def ContinuousMap.compStarAlgHom'

added theorem ContinuousMap.compStarAlgHom'_comp

added theorem ContinuousMap.compStarAlgHom'_id

added theorem ContinuousMap.div_apply

added theorem ContinuousMap.div_comp

added theorem ContinuousMap.hasSum_apply

added theorem ContinuousMap.inf_eq

added theorem ContinuousMap.int_cast_apply

added theorem ContinuousMap.inv_apply

added theorem ContinuousMap.inv_comp

added theorem ContinuousMap.mul_apply

added theorem ContinuousMap.mul_comp

added theorem ContinuousMap.nat_cast_apply

added theorem ContinuousMap.one_apply

added theorem ContinuousMap.one_comp

added theorem ContinuousMap.periodic_tsum_comp_add_zsmul

added theorem ContinuousMap.pow_apply

added theorem ContinuousMap.pow_comp

added theorem ContinuousMap.prod_apply

added theorem ContinuousMap.smul_apply

added theorem ContinuousMap.smul_comp

added theorem ContinuousMap.star_apply

added theorem ContinuousMap.summable_apply

added theorem ContinuousMap.sup_eq

added theorem ContinuousMap.tsum_apply

added theorem ContinuousMap.zpow_apply

added theorem ContinuousMap.zpow_comp

added def Homeomorph.compStarAlgEquiv'

added def Set.SeparatesPointsStrongly

added theorem Subalgebra.SeparatesPoints.strongly

added theorem Subalgebra.separatesPoints_monotone

added theorem algebraMap_apply

added def continuousSubalgebra

added def continuousSubgroup

added def continuousSubmodule

added def continuousSubmonoid

added def continuousSubring

added def continuousSubsemiring

added theorem max_eq_half_add_add_abs_sub

added theorem min_eq_half_add_sub_abs_sub