Functional dependency

Conjectura.Defs.ComputerScience.Databases.FunctionalDependency

/-
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
-/
import Conjectura.Defs.ComputerScience.Databases.RelationInstance

/-! # Functional dependency -/

namespace Conjectura.Databases

/-- A **functional dependency** `X → Y` holds when any two tuples agreeing on every
attribute in `X` also agree on every attribute in `Y`. Normalisation theory is the
study of which dependencies a schema forces. -/
def Satisfies {Attr Val : Type*} (r : RelationInstance Attr Val)
    (X Y : Set Attr) : Prop :=
  ∀ t ∈ r, ∀ u ∈ r, (∀ a ∈ X, t a = u a) → ∀ b ∈ Y, t b = u b

end Conjectura.Databases