Theorems · Theorem · general topology

Homeomorph.sumArrowHomeomorphProdArrow_symm_apply

∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_7} {ι' : Type u_8} (p : (ι → X) × (ι' → X)) (a : ι ⊕ ι'),
  Homeomorph.sumArrowHomeomorphProdArrow.symm p a = Sum.elim p.1 p.2 a

Defined in

Mathlib.Topology.Homeomorph.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace