Commit 2023-02-02 17:16 2fcb0697

View on Github →

feat: port Topology.Algebra.ConstMulAction (#2012)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/ConstMulAction.lean

added theorem Continuous.const_smul

added theorem ContinuousOn.const_smul

added theorem Dense.smul

added theorem Filter.Tendsto.const_smul

added theorem HasCompactMulSupport.comp_smul

added theorem HasCompactSupport.comp_smul

added theorem HasContinuousConstSmul.secondCountableTopology

added def Homeomorph.smul

added theorem IsClosed.smul

added theorem IsClosed.smul_of_ne_zero

added theorem IsClosed.smul₀

added theorem IsCompact.smul

added theorem IsOpen.smul

added theorem IsOpen.smul₀

added theorem closure_smul

added theorem closure_smul₀

added theorem continuousAt_const_smul_iff

added theorem continuousAt_const_smul_iff₀

added theorem continuousOn_const_smul_iff

added theorem continuousOn_const_smul_iff₀

added theorem continuousWithinAt_const_smul_iff

added theorem continuousWithinAt_const_smul_iff₀

added theorem continuous_const_smul_iff

added theorem continuous_const_smul_iff₀

added theorem interior_smul

added theorem interior_smul₀

added theorem isClosedMap_smul

added theorem isClosedMap_smul_of_ne_zero

added theorem isClosedMap_smul₀

added theorem isOpenMap_quotient_mk'_mul

added theorem isOpenMap_smul

added theorem isOpenMap_smul₀

added theorem set_smul_mem_nhds_smul

added theorem set_smul_mem_nhds_smul_iff

added theorem set_smul_mem_nhds_zero_iff

added theorem smul_closure_orbit_subset

added theorem smul_closure_subset

added theorem tendsto_const_smul_iff

added theorem tendsto_const_smul_iff₀