Theorems · Theorem · general topology

ContinuousMap.continuousOn_mkD_of_uncurry

∀ {X : Type u_2} {Y : Type u_3} {T : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace T] {s : Set T} (f : T → X → Y) (g : C(X, Y)),
  ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ) → ContinuousOn (fun x => ContinuousMap.mkD (f x) g) s

Defined in: Mathlib.Topology.CompactOpen
Cited by: 1 results in Mathlib
Foundations: Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites18

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

DFunLike.coeproof · cited by 62,936
Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Set.Elemproof · cited by 7,166
Set.univstatement and proof · cited by 3,945
Continuousproof · cited by 2,592
ContinuousMapstatement and proof · cited by 2,491
SProd.sprodstatement and proof · cited by 1,750
ContinuousOnstatement and proof · cited by 1,411
continuous_idproof · cited by 192
continuous_subtype_valproof · cited by 159
Continuous.prodMk_rightproof · cited by 32

Cited by1

Results whose statement or proof uses this declaration.

ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurryproof · cited by 1