Theorems · Theorem · general topology

Path.mul_apply

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Mul X] [inst_2 : ContinuousMul X] {a₁ b₁ a₂ b₂ : X}
  (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) (a : ↑unitInterval), (γ₁.mul γ₂) a = γ₁ a * γ₂ a

Defined in

Mathlib.Topology.Path

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMulContinuousMul