Theorems · Theorem · global analysis

boundary_product

∀ {x y : ℝ} [hxy : Fact (x < y)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
  [inst_2 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [I.Boundaryless], ModelWithCorners.boundary (M × ↑(Set.Icc x y)) = Set.univ.prod {⊥, ⊤}

A product M × [x,y] for M boundaryless has boundary M × {x, y}.

Defined in

Mathlib.Geometry.Manifold.Instances.Real

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceModelWithCorners.Boundaryless