Formal concept analysis

This file defines concept lattices. A concept of a relation r : α → β → Prop is a pair of sets s : Set α and t : Set β such that s is the set of all a : α that are related to all elements of t, and t is the set of all b : β that are related to all elements of s.

Ordering the concepts of a relation r by inclusion on the first component gives rise to a concept lattice. Every concept lattice is complete and in fact every complete lattice arises as the concept lattice of its ≤.

Implementation notes

Concept lattices are usually defined from a context, that is the triple (α, β, r), but the type of r determines α and β already, so we do not define contexts as a separate object.

TODO

Prove the fundamental theorem of concept lattices.

References

• [Davey, Priestley Introduction to Lattices and Order][davey_priestley]

Tags

concept, formal concept analysis, intent, extend, attribute

Intent and extent

def intentClosure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : Set β

The intent closure of s : Set α along a relation r : α → β → Prop is the set of all elements which r relates to all elements of s.

Equations

• intentClosure r s = {b : β | ∀ ⦃a : α⦄, a ∈ s → r a b}

def extentClosure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : Set α

The extent closure of t : Set β along a relation r : α → β → Prop is the set of all elements which r relates to all elements of t.

Equations

• extentClosure r t = {a : α | ∀ ⦃b : β⦄, b ∈ t → r a b}

theorem subset_intentClosure_iff_subset_extentClosure {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} {t : Set β} : t ⊆ intentClosure r s ↔ s ⊆ extentClosure r t

theorem gc_intentClosure_extentClosure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : GaloisConnection (⇑OrderDual.toDual ∘ intentClosure r) (extentClosure r ∘ ⇑OrderDual.ofDual)

theorem intentClosure_swap {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : intentClosure (Function.swap r) t = extentClosure r t

theorem extentClosure_swap {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : extentClosure (Function.swap r) s = intentClosure r s

@[simp]

theorem intentClosure_empty {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : intentClosure r ∅ = Set.univ

@[simp]

theorem extentClosure_empty {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : extentClosure r ∅ = Set.univ

@[simp]

theorem intentClosure_union {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s₁ : Set α) (s₂ : Set α) : intentClosure r (s₁ ∪ s₂) = intentClosure r s₁ ∩ intentClosure r s₂

@[simp]

theorem extentClosure_union {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t₁ : Set β) (t₂ : Set β) : extentClosure r (t₁ ∪ t₂) = extentClosure r t₁ ∩ extentClosure r t₂

@[simp]

theorem intentClosure_iUnion {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (f : ι → Set α) : intentClosure r (⋃ (i : ι), f i) = ⋂ (i : ι), intentClosure r (f i)

@[simp]

theorem extentClosure_iUnion {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (f : ι → Set β) : extentClosure r (⋃ (i : ι), f i) = ⋂ (i : ι), extentClosure r (f i)

theorem intentClosure_iUnion₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} (r : α → β → Prop) (f : (i : ι) → κ i → Set α) : intentClosure r (⋃ (i : ι), ⋃ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), intentClosure r (f i j)

theorem extentClosure_iUnion₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} (r : α → β → Prop) (f : (i : ι) → κ i → Set β) : extentClosure r (⋃ (i : ι), ⋃ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), extentClosure r (f i j)

theorem subset_extentClosure_intentClosure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : s ⊆ extentClosure r (intentClosure r s)

theorem subset_intentClosure_extentClosure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : t ⊆ intentClosure r (extentClosure r t)

@[simp]

theorem intentClosure_extentClosure_intentClosure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : intentClosure r (extentClosure r (intentClosure r s)) = intentClosure r s

@[simp]

theorem extentClosure_intentClosure_extentClosure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : extentClosure r (intentClosure r (extentClosure r t)) = extentClosure r t

theorem intentClosure_anti {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : Antitone (intentClosure r)

theorem extentClosure_anti {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : Antitone (extentClosure r)

Concepts

structure Concept (α : Type u_2) (β : Type u_3) (r : α → β → Prop) extends Prod : Type (max u_2 u_3)

The formal concepts of a relation. A concept of r : α → β → Prop is a pair of sets s, t such that s is the set of all elements that are r-related to all of t and t is the set of all elements that are r-related to all of s.

• fst : Set α
• snd : Set β
• closure_fst : intentClosure r self.toProd.1 = self.toProd.2

  The axiom of a Concept stating that the closure of the first set is the second set.

• closure_snd : extentClosure r self.toProd.2 = self.toProd.1

  The axiom of a Concept stating that the closure of the second set is the first set.

theorem Concept.ext {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {d : Concept α β r} (h : c.toProd.1 = d.toProd.1) : c = d

theorem Concept.ext' {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {d : Concept α β r} (h : c.toProd.2 = d.toProd.2) : c = d

theorem Concept.fst_injective {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Function.Injective fun (c : Concept α β r) => c.toProd.1

theorem Concept.snd_injective {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Function.Injective fun (c : Concept α β r) => c.toProd.2

instance Concept.instSupConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Sup (Concept α β r)

Equations

• One or more equations did not get rendered due to their size.

instance Concept.instInfConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Inf (Concept α β r)

Equations

• One or more equations did not get rendered due to their size.

instance Concept.instSemilatticeInfConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : SemilatticeInf (Concept α β r)

Equations

• Concept.instSemilatticeInfConcept = Function.Injective.semilatticeInf (fun (c : Concept α β r) => c.toProd.1) ⋯ ⋯

@[simp]

theorem Concept.fst_subset_fst_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {d : Concept α β r} : c.toProd.1 ⊆ d.toProd.1 ↔ c ≤ d

@[simp]

theorem Concept.fst_ssubset_fst_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {d : Concept α β r} : c.toProd.1 ⊂ d.toProd.1 ↔ c < d

@[simp]

theorem Concept.snd_subset_snd_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {d : Concept α β r} : c.toProd.2 ⊆ d.toProd.2 ↔ d ≤ c

@[simp]

theorem Concept.snd_ssubset_snd_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {d : Concept α β r} : c.toProd.2 ⊂ d.toProd.2 ↔ d < c

theorem Concept.strictMono_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : StrictMono (Prod.fst ∘ Concept.toProd)

theorem Concept.strictAnti_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : StrictAnti (Prod.snd ∘ Concept.toProd)

instance Concept.instLatticeConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Lattice (Concept α β r)

Equations

• Concept.instLatticeConcept = let __src := Concept.instSemilatticeInfConcept; Lattice.mk ⋯ ⋯ ⋯

instance Concept.instBoundedOrderConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : BoundedOrder (Concept α β r)

Equations

• Concept.instBoundedOrderConcept = BoundedOrder.mk

instance Concept.instSupSetConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : SupSet (Concept α β r)

Equations

• Concept.instSupSetConcept = { sSup := fun (S : Set (Concept α β r)) => { toProd := (extentClosure r (⋂ c ∈ S, c.toProd.2), ⋂ c ∈ S, c.toProd.2), closure_fst := ⋯, closure_snd := ⋯ } }

instance Concept.instInfSetConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : InfSet (Concept α β r)

Equations

• Concept.instInfSetConcept = { sInf := fun (S : Set (Concept α β r)) => { toProd := (⋂ c ∈ S, c.toProd.1, intentClosure r (⋂ c ∈ S, c.toProd.1)), closure_fst := ⋯, closure_snd := ⋯ } }

instance Concept.instCompleteLatticeConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : CompleteLattice (Concept α β r)

Equations

• Concept.instCompleteLatticeConcept = let __src := Concept.instLatticeConcept; let __src_1 := Concept.instBoundedOrderConcept; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Concept.top_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊤.toProd.1 = Set.univ

@[simp]

theorem Concept.top_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊤.toProd.2 = intentClosure r Set.univ

@[simp]

theorem Concept.bot_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊥.toProd.1 = extentClosure r Set.univ

@[simp]

theorem Concept.bot_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊥.toProd.2 = Set.univ

@[simp]

theorem Concept.sup_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (d : Concept α β r) : (c ⊔ d).toProd.1 = extentClosure r (c.toProd.2 ∩ d.toProd.2)

@[simp]

theorem Concept.sup_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (d : Concept α β r) : (c ⊔ d).toProd.2 = c.toProd.2 ∩ d.toProd.2

@[simp]

theorem Concept.inf_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (d : Concept α β r) : (c ⊓ d).toProd.1 = c.toProd.1 ∩ d.toProd.1

@[simp]

theorem Concept.inf_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (d : Concept α β r) : (c ⊓ d).toProd.2 = intentClosure r (c.toProd.1 ∩ d.toProd.1)

@[simp]

theorem Concept.sSup_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sSup S).toProd.1 = extentClosure r (⋂ c ∈ S, c.toProd.2)

@[simp]

theorem Concept.sSup_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sSup S).toProd.2 = ⋂ c ∈ S, c.toProd.2

@[simp]

theorem Concept.sInf_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sInf S).toProd.1 = ⋂ c ∈ S, c.toProd.1

@[simp]

theorem Concept.sInf_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sInf S).toProd.2 = intentClosure r (⋂ c ∈ S, c.toProd.1)

instance Concept.instInhabitedConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Inhabited (Concept α β r)

Equations

• Concept.instInhabitedConcept = { default := ⊥ }

@[simp]

theorem Concept.swap_toProd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : (Concept.swap c).toProd = Prod.swap c.toProd

def Concept.swap {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : Concept β α (Function.swap r)

Swap the sets of a concept to make it a concept of the dual context.

Equations

• Concept.swap c = { toProd := Prod.swap c.toProd, closure_fst := ⋯, closure_snd := ⋯ }

@[simp]

theorem Concept.swap_swap {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : Concept.swap (Concept.swap c) = c

@[simp]

theorem Concept.swap_le_swap_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {d : Concept α β r} : Concept.swap c ≤ Concept.swap d ↔ d ≤ c

@[simp]

theorem Concept.swap_lt_swap_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {d : Concept α β r} : Concept.swap c < Concept.swap d ↔ d < c

@[simp]

theorem Concept.swapEquiv_symm_apply {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ∀ (a : Concept β α (Function.swap r)), (RelIso.symm Concept.swapEquiv) a = (⇑OrderDual.toDual ∘ Concept.swap) a

@[simp]

theorem Concept.swapEquiv_apply {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ∀ (a : (Concept α β r)ᵒᵈ), Concept.swapEquiv a = (Concept.swap ∘ ⇑OrderDual.ofDual) a

def Concept.swapEquiv {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : (Concept α β r)ᵒᵈ ≃o Concept β α (Function.swap r)

The dual of a concept lattice is isomorphic to the concept lattice of the dual context.

Equations

• Concept.swapEquiv = { toEquiv := { toFun := Concept.swap ∘ ⇑OrderDual.ofDual, invFun := ⇑OrderDual.toDual ∘ Concept.swap, left_inv := ⋯, right_inv := ⋯ }, map_rel_iff' := ⋯ }