Theorems · Theorem · Lie groups

ContinuousWithinAt.pow

∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Monoid M]
  [ContinuousMul M] {f : X → M} {x : X} {s : Set X},
  ContinuousWithinAt f s x → ∀ (n : ℕ), ContinuousWithinAt (f ^ n) s x

Defined in: Mathlib.Topology.Algebra.Monoid
Cited by: 3 results in Mathlib
Foundations: Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace Monoid ContinuousMul

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Monoidstatement and proof · cited by 3,887
ContinuousWithinAtstatement and proof · cited by 512
ContinuousMulstatement and proof · cited by 343
Filter.Tendsto.powproof · cited by 16

Cited by3

Results whose statement or proof uses this declaration.

ContinuousOn.powproof · cited by 4
BoxIntegral.hasIntegral_GP_pderivproof · cited by 1
ContinuousWithinAt.fun_powproof · cited by 0