Theorems · Theorem · Lie groups

RestrictedProduct.mapAlong_continuous

∀ {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) [inst : (i : ι₁) → TopologicalSpace (R₁ i)]
  [inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)}
  {A₂ : (i : ι₂) → Set (R₂ i)} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) (φ : (j : ι₂) → R₁ (f j) → R₂ j)
  (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo (φ j) (A₁ (f j)) (A₂ j)),
  (∀ (j : ι₂), Continuous (φ j)) → Continuous (RestrictedProduct.mapAlong R₁ R₂ f hf φ hφ)

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace