Counting finite incidences by target labels
DefinitionEsgk_FiniteIncidenceCodegreeBoundfinite-combinatoricsincidence-geometry
This counts pairs in finite source and target sets satisfying a given relation by summing the filtered source cardinalities over target labels.
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.
-/
noncomputable section
open scoped Classical
namespace Esgk
def finiteIncidenceCount {α β : Type*}
(P : Finset α) (C : Finset β) (R : α → β → Prop) : ℕ := by
classical
exact ∑ b ∈ C, (P.filter (fun x ↦ R x b)).card
end Esgk