ComplementComponent
DefinitionComplementComponentcrossing-consequencesgeometrypolygonal
A connected component of the complement of a set: a nonempty connected subset of the complement that is maximal among nonempty connected subsets of that complement.
Definition code
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Set.Finite.Basic
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
-- [TABLET NODE: ComplementComponent]
-- Source: https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/ComplementComponent.lean#L1-8
def ComplementComponent (K F : Set (EuclideanSpace ℝ (Fin 2))) : Prop :=
F.Nonempty ∧ F ⊆ Kᶜ ∧ IsConnected F ∧
∀ C : Set (EuclideanSpace ℝ (Fin 2)),
C.Nonempty → C ⊆ Kᶜ → IsConnected C → F ⊆ C → C ⊆ F
Source