pith. machine review for the scientific record. sign in
class definition def or abbrev

ConfigSpace

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  77class ConfigSpace (Config : Type u) where
  78  /-- The empty configuration. -/
  79  emp : Config
  80  /-- Joining two configurations. -/
  81  join : Config → Config → Config
  82  /-- Consistency: the configuration is jointly satisfiable. -/
  83  IsConsistent : Config → Prop
  84  /-- Independence: the two configurations share no predicates. -/
  85  Independent : Config → Config → Prop
  86  /-- Empty configuration is consistent. -/
  87  emp_consistent : IsConsistent emp
  88  /-- Independence is symmetric. -/
  89  independent_symm : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ → Independent Γ₂ Γ₁
  90  /-- Empty configuration is independent of every configuration. -/
  91  emp_independent : ∀ Γ, Independent emp Γ
  92  /-- Joining is commutative. -/
  93  join_comm : ∀ Γ₁ Γ₂, join Γ₁ Γ₂ = join Γ₂ Γ₁
  94  /-- Joining is associative. -/
  95  join_assoc : ∀ Γ₁ Γ₂ Γ₃, join (join Γ₁ Γ₂) Γ₃ = join Γ₁ (join Γ₂ Γ₃)
  96  /-- Empty is the join identity on the left. -/
  97  emp_join : ∀ Γ, join emp Γ = Γ
  98  /-- Joining two independent consistent configurations yields a
  99      consistent configuration. -/
 100  consistent_of_join_indep : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ →
 101    IsConsistent Γ₁ → IsConsistent Γ₂ → IsConsistent (join Γ₁ Γ₂)
 102  /-- If either side of an independent join is inconsistent, the join
 103      is inconsistent. (Independent inconsistencies do not cancel.) -/
 104  inconsistent_of_join_indep_left : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ →
 105    ¬IsConsistent Γ₁ → ¬IsConsistent (join Γ₁ Γ₂)
 106
 107namespace ConfigSpace
 108
 109variable {Config : Type u} [ConfigSpace Config]
 110
 111/-- Empty is the join identity on the right. -/

used by (25)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (20)

Lean names referenced from this declaration's body.