Mathlib Map

Theorems · Theorem · Lie groups

AddUnits.continuous_val

∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M], Continuous AddUnits.val
Defined in
Mathlib.Topology.Algebra.Constructions
Cited by
3 results in Mathlib
Foundations
Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpaceAddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AddUnits.continuous_map · cited by 2AddUnits.continuous_mapContinuous.addUnits_map · cited by 0Continuous.addUnits_mapAddSubmonoid.isOpen_addUnits · cited by 0AddSubmonoid.isOpen_addUn…TopologicalSpace · cited by 24529TopologicalSpaceAddMonoid · cited by 2864AddMonoidContinuous · cited by 2592ContinuousAddUnits · cited by 325AddUnitsAddUnits.val · cited by 248AddUnits.valContinuous.fst · cited by 73Continuous.fstAddUnits.continuous_embedProduct · cited by 3AddUnits.continuous_embed…AddUnits.continuous_valCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by3

Results whose statement or proof uses this declaration.