Theorems · Theorem · Lie groups
continuous_zero
∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Zero M],
Continuous 0- Defined in
- Mathlib.Topology.Algebra.Monoid
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Continuousstatement · cited by 2,592
- continuous_constproof · cited by 278
Cited by22
Results whose statement or proof uses this declaration.
- cfcₙ_zeroproof · cited by 7
- cfc_zeroproof · cited by 4
- AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNEproof · cited by 4
- Continuous.matrix_blockDiagonalproof · cited by 3
- Continuous.matrix_diagonalproof · cited by 3
- MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaarproof · cited by 3
- LinearMap.continuous_of_isClosed_kerproof · cited by 2
- MeasureTheory.continuous_L1_toL1proof · cited by 1
- Real.continuous_posLogproof · cited by 1
- spectrum_star_mul_self_nonnegproof · cited by 1
- IsSelfAdjoint.map_spectrum_realproof · cited by 1
- ContinuousMapZero.mul_nonUnitalStarAlgHom_apply_eq_zeroproof · cited by 1