Commit 2026-01-28 19:17 ba0a0a14

View on Github →

feat: add a typeclass for the indiscrete topology (#29120) Notably, this changes the assumptions of theorem ContinuousLinearMap.norm_id : ‖id 𝕜 E‖ = 1 from [NormedAddCommGroup E] [Nontrivial E] to the more general [SeminormedAddCommGroup E] [NontrivialTopology E]. As discussed in #Is there code for X? > Typeclass for nontrivial topology @ 💬 and #Is there code for X? > Typeclass for indiscrete topology @ 💬

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem IndiscreteTopology.nnnorm_eq_zero'

added theorem IndiscreteTopology.norm_eq_zero'

added theorem exists_nnnorm_ne_zero'

added theorem exists_norm_ne_zero'

added theorem indiscreteTopology_iff_forall_nnnorm_eq_zero'

added theorem indiscreteTopology_iff_forall_norm_eq_zero'

added theorem nontrivialTopology_iff_exists_nnnorm_ne_zero'

added theorem nontrivialTopology_iff_exists_norm_ne_zero'

Modified Mathlib/Analysis/Normed/Group/Hom.lean

modified theorem NormedAddGroupHom.norm_id

Modified Mathlib/Analysis/Normed/Group/SeparationQuotient.lean

modified theorem SeparationQuotient.norm_normedMk_eq_one

Modified Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean

Modified Mathlib/Analysis/Normed/Module/RCLike/Real.lean

Modified Mathlib/Analysis/Normed/Operator/Basic.lean

added theorem ContinuousLinearMap.homothety_norm

added theorem ContinuousLinearMap.nnnorm_id

added theorem ContinuousLinearMap.norm_id

Modified Mathlib/Analysis/Normed/Operator/Bilinear.lean

Modified Mathlib/Analysis/Normed/Operator/NormedSpace.lean

deleted theorem ContinuousLinearMap.homothety_norm

deleted theorem ContinuousLinearMap.nnnorm_id

deleted theorem ContinuousLinearMap.norm_id

Modified Mathlib/Topology/EMetricSpace/Basic.lean

added theorem EMetric.nontrivial_iff_nontrivialTopology

added theorem EMetric.subsingleton_iff_indiscreteTopology

Modified Mathlib/Topology/Homeomorph/Defs.lean

added theorem Homeomorph.indiscreteTopology_iff

added theorem Homeomorph.nontrivialTopology_iff

Modified Mathlib/Topology/Inseparable.lean

modified theorem SeparationQuotient.inseparableSetoid_eq_top_iff

modified theorem SeparationQuotient.nontrivial_iff

modified theorem SeparationQuotient.subsingleton_iff

Modified Mathlib/Topology/Maps/Basic.lean

added theorem Topology.IsInducing.indiscreteTopology

added theorem Topology.IsInducing.nontrivialTopology

Modified Mathlib/Topology/Order.lean

added theorem IndiscreteTopology.isOpen_iff

added theorem IndiscreteTopology.nhds_eq

added theorem IndiscreteTopology.of_forall_inseparable

added theorem Inseparable.all

added theorem TopologicalSpace.indiscrete_iff_forall_inseparable

added theorem TopologicalSpace.indiscrete_or_nontrivial

added theorem TopologicalSpace.nontrivial_iff_exists_not_inseparable

added theorem TopologicalSpace.not_indiscrete_iff

added theorem TopologicalSpace.not_nontrivial_iff

modified theorem inseparable_top

Modified Mathlib/Topology/Sets/Opens.lean

modified theorem TopologicalSpace.Opens.eq_bot_or_top

Modified Mathlib/Topology/Sheaves/PUnit.lean