Relation instance

RelationInstanceabbrev

A relation instance in the sense of the relational model: a finite set of tuples over a fixed attribute type. This is the object every query language in database theory manipulates.

abbrev RelationInstance (Attr Val : Type*) := Set (Attr → Val)

Used by

Conjunctive query
Functional dependency

From Mathlib

Data.Finset.Card
Data.Set.Defs

import Conjectura.Defs.ComputerScience.Databases.RelationInstance · maintainer — open · raw source

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

Full credits