Mathlib Map

Theorems · Theorem · general topology

ContinuousAt.snd

∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y × Z} {x : X}, ContinuousAt f x → ContinuousAt (fun x => (f x).2) x

Postcomposing f with Prod.snd is continuous at x

Defined in
Mathlib.Topology.Constructions.SumProd
Cited by
9 results in Mathlib
Foundations
Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpaceTopologicalSpaceTopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

mapClusterPt_self_zpow_atTop_pow · cited by 3mapClusterPt_self_zpow_at…mapClusterPt_self_zsmul_atTop_nsmul · cited by 3mapClusterPt_self_zsmul_a…Real.continuousAt_rpow_of_ne · cited by 2Real.continuousAt_rpow_of…EuclideanGeometry.continuousAt_oangle · cited by 2EuclideanGeometry.continu…NNReal.continuousAt_rpow · cited by 1NNReal.continuousAt_rpowintegral_log_from_zero_of_pos · cited by 1integral_log_from_zero_of…Complex.continuousAt_ofReal_cpow · cited by 1Complex.continuousAt_ofRe…InnerProductGeometry.continuousAt_angle · cited by 1InnerProductGeometry.cont…EuclideanGeometry.continuousAt_angle · cited by 0EuclideanGeometry.continu…TopologicalSpace · cited by 24529TopologicalSpaceContinuousAt · cited by 697ContinuousAtContinuousAt.comp · cited by 56ContinuousAt.compcontinuousAt_snd · cited by 12continuousAt_sndContinuousAt.sndCITED BYCITES

Cites4

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

Cited by9

Results whose statement or proof uses this declaration.