Theorems · Theorem · algebraic topology

OpenPartialHomeomorph.piecewise.congr_simp

∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e_1 : OpenPartialHomeomorph X Y) (e_e : e = e_1) (e' e'_1 : OpenPartialHomeomorph X Y) (e_e' : e' = e'_1)
  (s s_1 : Set X) (e_s : s = s_1) (t t_1 : Set Y) (e_t : t = t_1) {inst_2 : (x : X) → Decidable (x ∈ s)}
  [inst_3 : (x : X) → Decidable (x ∈ s_1)] {inst_4 : (y : Y) → Decidable (y ∈ t)}
  [inst_5 : (y : Y) → Decidable (y ∈ t_1)] (H : e.IsImage s t) (H' : e'.IsImage s t)
  (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)),
  e.piecewise e' s t H H' Hs Heq = e_1.piecewise e'_1 s_1 t_1 ⋯ ⋯ ⋯ ⋯

Defined in

Mathlib.Topology.FiberBundle.Trivialization

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceDecidableDecidable