OAI/Analysis/CoulombTransport/ComponentRegions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.SmoothBranchMarginal.componentRegion_pairwise_of_subsets line 11

   Source documentation

   Component containment in the disjoint five certificate regions supplies exactly the disjointness input of the smooth marginal construction.

   theorem componentRegion_pairwise_of_subsets
       {B : Set E3} {e : Fin 4 → OpenPartialHomeomorph E3 E3}
       {U : Fin 5 → Set E3}
       (hU : Pairwise (fun i j => Disjoint (U i) (U j)))
       (hB : B ⊆ U 0) (he : ∀ i, e i '' B ⊆ U i.succ) :
       Pairwise (fun i j => Disjoint (componentRegion B e i) (componentRegion B e j)) := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.SmoothBranchMarginal.componentRegion