Mathlib Map

Theorems · Theorem · Lie groups

continuousMul_sInf

∀ {M : Type u_3} [inst : Mul M] {ts : Set (TopologicalSpace M)}, (∀ t ∈ ts, ContinuousMul M) → ContinuousMul M
Defined in
Mathlib.Topology.Algebra.Monoid
Cited by
2 results in Mathlib
Foundations
Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Mul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

continuousMul_iInf · cited by 1continuousMul_iInftopologicalGroup_sInf · cited by 1topologicalGroup_sInfSet · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceInfSet.sInf · cited by 935InfSet.sInfContinuousMul · cited by 343ContinuousMulcontinuous_sInf_rng · cited by 9continuous_sInf_rngcontinuous_sInf_dom₂ · cited by 4continuous_sInf_dom₂ContinuousMul.continuous_mul · cited by 3ContinuousMul.continuous_…continuousMul_sInfCITED BYCITES

Cites7

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

Cited by2

Results whose statement or proof uses this declaration.