Shattering

Shattersdef

A binary concept class shatters a set when every one of its subsets is cut out by some concept — the class can realise every possible labelling of those points.

def Shatters {α : Type*} (C : ConceptClass α Bool) (W : Set α) : Prop :=
  ∀ W' ⊆ W, ∃ c ∈ C, ∀ x ∈ W, (c x = true ↔ x ∈ W')

Builds on

Concept class

Used by

Finite VC dimension
VC dimension

import Conjectura.Defs.ComputerScience.Learning.Shatters · maintainer — open · raw source

Adapted for Conjectura from cslib, split into one concept per module. Released by its authors under Apache 2.0.

Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger

Full credits