Conjectura
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Concept class

Conjectura.Defs.ComputerScience.Learning.ConceptClass

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

/-! # Concept class

## Source

Adapted for Conjectura from [cslib](https://github.com/leanprover/cslib), split into one concept per module. Released by its authors under Apache 2.0.
-/

namespace Conjectura.Learning

/-- A **concept class** over a domain `α` with labels in `β` is a set of functions `α → β` —
the hypotheses a learner is allowed to consider. For binary labels it is equivalently a family
of subsets of `α`. -/
abbrev ConceptClass (α β : Type*) := Set (α → β)

end Conjectura.Learning