Theorems · Definition · general topology

Path.prod

{X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {a₁ a₂ : X} → {b₁ b₂ : Y} → Path a₁ a₂ → Path b₁ b₂ → Path (a₁, b₁) (a₂, b₂)

Given a path in X and a path in Y, we can take their pointwise product to get a path in X × Y.

Defined in

Mathlib.Topology.Path

Cited by

9 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace