Theorems · Theorem · general topology
Path.continuous_uncurry_iff
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {Y : Type u_4} [inst_1 : TopologicalSpace Y] {g : Y → Path x y},
Continuous ↿g ↔ Continuous g- Defined in
- Mathlib.Topology.Path
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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 · cited by 53,352
- Realstatement · cited by 25,697
- TopologicalSpacestatement and proof · cited by 24,529
- Set.Elemstatement · cited by 7,166
- Continuousstatement and proof · cited by 2,592
- unitIntervalstatement · cited by 607
- Pathstatement and proof · cited by 318
- ContinuousMapClass.map_continuousproof · cited by 119
- toContinuousMapproof · cited by 99
- Function.HasUncurry.uncurrystatement · cited by 57
- continuous_induced_rngproof · cited by 38
Cited by4
Results whose statement or proof uses this declaration.
- Path.continuous_symmproof · cited by 1
- Path.continuous_delayReflRightproof · cited by 1
- Continuous.path_transproof · cited by 1
- GenLoop.continuous_toLoopproof · cited by 0