Theorems · Theorem · general topology

JoinedIn.mul

∀ {M : Type u_4} [inst : Mul M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {s t : Set M} {a b c d : M},
  JoinedIn s a b → JoinedIn t c d → JoinedIn (s * t) (a * c) (b * d)

Defined in

Mathlib.Topology.Connected.PathConnected

Cited by

1 results in Mathlib

Foundations

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

Assumes

MulTopologicalSpaceContinuousMul