Theorems · Theorem · general topology

equicontinuousAt_iInf_rng

∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α' : Type u_7} [tX : TopologicalSpace X] {u : κ → UniformSpace α'}
  {F : ι → X → α'} {x₀ : X}, EquicontinuousAt F x₀ ↔ ∀ (k : κ), EquicontinuousAt F x₀

Defined in

Mathlib.Topology.UniformSpace.Equicontinuity

Cited by

1 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace