A selected connected component on one side of a boundary
DefinitionEsgk_FiniteBoundaryCurveComponentsreal-analysistopology
This chooses the connected component of an open set containing a chosen point of its intersection with another set, returning the empty set when that intersection is empty.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Mathlib
/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/
noncomputable section
open Set
open scoped Classical
namespace Esgk
variable {M : Type*} [TopologicalSpace M] [T1Space M]
omit [T1Space M] in
def bundle_Esgk_FiniteBoundaryCurveComponents_chosenSideComponent (U A : Set M) : Set M :=
if h : (A ∩ U).Nonempty then connectedComponentIn U h.choose else ∅
end Esgk