Mathlib Map

Theorems · Definition · general topology

Joined.somePath

{X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → Joined x y → Path x y

When two points are joined, choose some path from x to y.

Defined in
Mathlib.Topology.Connected.PathConnected
Cited by
12 results in Mathlib
Foundations
Depth 3 from the axioms · uses Classical.choice
Assumes
TopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Joined.trans · cited by 4Joined.transJoined.symm · cited by 3Joined.symmJoined.map · cited by 2Joined.mapJoined.mul · cited by 2Joined.mulpathComponent_subset_component · cited by 2pathComponent_subset_comp…Joined.add · cited by 1Joined.addJoined.pi · cited by 1Joined.piJoined.prod · cited by 1Joined.prodJoined.inv · cited by 0Joined.invJoined.somePath.congr_simp · cited by 0somePath.congr_simpJoined.neg · cited by 0Joined.negjoinedIn_iff_joined · cited by 0joinedIn_iff_joinedTopologicalSpace · cited by 24529TopologicalSpaceNonempty.some · cited by 340Nonempty.somePath · cited by 318PathJoined · cited by 29JoinedJoined.somePathCITED BYCITES

Cites4

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

Cited by12

Results whose statement or proof uses this declaration.