Theorems · Theorem · general topology

ContinuousMap.concat_comp_IccInclusionLeft

∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b c : α}
  [inst_3 : Fact (a ≤ b)] [inst_4 : Fact (b ≤ c)] {E : Type u_2} [inst_5 : TopologicalSpace E]
  {f : C(↑(Set.Icc a b), E)} {g : C(↑(Set.Icc b c), E)},
  f ⊤ = g ⊥ → (f.concat g).comp ContinuousMap.IccInclusionLeft = f

Defined in

Mathlib.Topology.ContinuousMap.Interval

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopologyFactFactTopologicalSpace