Deleting ordered pairs involving exceptional points

Definition

Esgk_SelfCurveDistancePairs

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

algebraic-geometrygeometry

For finite sets of sample and exceptional points, this defines the union of ordered pairs with one coordinate in each set. A second definition adds an arbitrary further set of ordered pairs to be deleted.

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
-/


namespace Esgk


def exceptionalOrderedPairs {α : Type*} [DecidableEq α]
    (S E : Finset α) : Finset (α × α) :=
  (E ×ˢ S) ∪ (S ×ˢ E)


def deletedIndexedPairs {α : Type*} [DecidableEq α]
    (S E : Finset α) (Γ : Finset (α × α)) : Finset (α × α) :=
  exceptionalOrderedPairs S E ∪ Γ


end Esgk

View graph