Open-cover data with a split overlap

Definition

LeanFormalizations_PachDeZeeuw_CrossingLemma_PLCover

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

topology

This records two open sets covering a topological space and a decomposition of their overlap into two disjoint open sets. It also equips the two-element residue ring with the discrete topology.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Mathlib

set_option autoImplicit true

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/

namespace CrossingLemma.PLCover

open Set Topology Bundle
open scoped Classical

universe u

 
instance : TopologicalSpace (ZMod 2) := ⊥
instance : DiscreteTopology (ZMod 2) := ⟨rfl⟩

variable {B : Type u} [TopologicalSpace B]


structure GlueData (B : Type u) [TopologicalSpace B] where
  V₀ : Set B
  V₁ : Set B
  Pp : Set B
  Pm : Set B
  isOpen_V₀ : IsOpen V₀
  isOpen_V₁ : IsOpen V₁
  isOpen_Pp : IsOpen Pp
  isOpen_Pm : IsOpen Pm
  cover : V₀ ∪ V₁ = univ
  overlap : V₀ ∩ V₁ = Pp ∪ Pm
  disjoint_Pp_Pm : Disjoint Pp Pm

namespace GlueData

variable (D : GlueData B)


end GlueData

end CrossingLemma.PLCover

View graph