Formal concept analysis #
This file defines concept lattices. A concept of a relation r : α → β → Prop→ β → Prop→ 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 #
The intent closure of s : Set α along a relation r : α → β → Prop→ β → Prop→ 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 }
The extent closure of t : Set β along a relation r : α → β → Prop→ β → Prop→ 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_1}
{r : α → β → Prop}
{s : Set α}
{t : Set β}
:
t ⊆ intentClosure r s ↔ s ⊆ extentClosure r t
theorem
gc_intentClosure_extentClosure
{α : Type u_1}
{β : Type u_2}
(r : α → β → Prop)
:
GaloisConnection (↑OrderDual.toDual ∘ intentClosure r) (extentClosure r ∘ ↑OrderDual.ofDual)
theorem
intentClosure_swap
{α : Type u_2}
{β : Type u_1}
(r : α → β → Prop)
(t : Set β)
:
intentClosure (Function.swap r) t = extentClosure r t
theorem
extentClosure_swap
{α : Type u_1}
{β : Type u_2}
(r : α → β → Prop)
(s : Set α)
:
extentClosure (Function.swap r) s = intentClosure r s
@[simp]
theorem
intentClosure_empty
{α : Type u_2}
{β : Type u_1}
(r : α → β → Prop)
:
intentClosure r ∅ = Set.univ
@[simp]
theorem
extentClosure_empty
{α : Type u_1}
{β : Type u_2}
(r : α → β → Prop)
:
extentClosure r ∅ = Set.univ
@[simp]
theorem
intentClosure_union
{α : Type u_1}
{β : Type u_2}
(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_1}
(r : α → β → Prop)
(t₁ : Set β)
(t₂ : Set β)
:
extentClosure r (t₁ ∪ t₂) = extentClosure r t₁ ∩ extentClosure r t₂
@[simp]
theorem
intentClosure_unionᵢ
{ι : Sort u_3}
{α : Type u_1}
{β : Type u_2}
(r : α → β → Prop)
(f : ι → Set α)
:
intentClosure r (Set.unionᵢ fun i => f i) = Set.interᵢ fun i => intentClosure r (f i)
@[simp]
theorem
extentClosure_unionᵢ
{ι : Sort u_3}
{α : Type u_2}
{β : Type u_1}
(r : α → β → Prop)
(f : ι → Set β)
:
extentClosure r (Set.unionᵢ fun i => f i) = Set.interᵢ fun i => extentClosure r (f i)
theorem
intentClosure_unionᵢ₂
{ι : Sort u_3}
{α : Type u_1}
{β : Type u_2}
{κ : ι → Sort u_4}
(r : α → β → Prop)
(f : (i : ι) → κ i → Set α)
:
intentClosure r (Set.unionᵢ fun i => Set.unionᵢ fun j => f i j) = Set.interᵢ fun i => Set.interᵢ fun j => intentClosure r (f i j)
theorem
extentClosure_Union₂
{ι : Sort u_3}
{α : Type u_2}
{β : Type u_1}
{κ : ι → Sort u_4}
(r : α → β → Prop)
(f : (i : ι) → κ i → Set β)
:
extentClosure r (Set.unionᵢ fun i => Set.unionᵢ fun j => f i j) = Set.interᵢ fun i => Set.interᵢ fun j => extentClosure r (f i j)
theorem
subset_extentClosure_intentClosure
{α : Type u_1}
{β : Type u_2}
(r : α → β → Prop)
(s : Set α)
:
s ⊆ extentClosure r (intentClosure r s)
theorem
subset_intentClosure_extentClosure
{α : Type u_2}
{β : Type u_1}
(r : α → β → Prop)
(t : Set β)
:
t ⊆ intentClosure r (extentClosure r t)
@[simp]
theorem
intentClosure_extentClosure_intentClosure
{α : Type u_1}
{β : Type u_2}
(r : α → β → Prop)
(s : Set α)
:
intentClosure r (extentClosure r (intentClosure r s)) = intentClosure r s
@[simp]
theorem
extentClosure_intentClosure_extentClosure
{α : Type u_2}
{β : Type u_1}
(r : α → β → Prop)
(t : Set β)
:
extentClosure r (intentClosure r (extentClosure r t)) = extentClosure r t
Concepts #
The axiom of a
Conceptstating that the closure of the first set is the second set.closure_fst : intentClosure r toProd.fst = toProd.sndThe axiom of a
Conceptstating that the closure of the second set is the first set.closure_snd : extentClosure r toProd.snd = toProd.fst
The formal concepts of a relation. A concept of r : α → β → Prop→ β → Prop→ 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.
Instances For
theorem
Concept.fst_injective
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
Function.Injective fun c => c.toProd.fst
theorem
Concept.snd_injective
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
Function.Injective fun c => c.toProd.snd
instance
Concept.instSemilatticeInfConcept
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
SemilatticeInf (Concept α β r)
Equations
- One or more equations did not get rendered due to their size.
theorem
Concept.strictMono_fst
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
StrictMono (Prod.fst ∘ Concept.toProd)
theorem
Concept.strictAnti_snd
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
StrictAnti (Prod.snd ∘ Concept.toProd)
instance
Concept.instBoundedOrderConceptToLEToPreorderToPartialOrderInstSemilatticeInfConcept
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
BoundedOrder (Concept α β r)
Equations
- Concept.instBoundedOrderConceptToLEToPreorderToPartialOrderInstSemilatticeInfConcept = BoundedOrder.mk
instance
Concept.instCompleteLatticeConcept
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
CompleteLattice (Concept α β r)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Concept.top_snd
{α : Type u_2}
{β : Type u_1}
{r : α → β → Prop}
:
⊤.toProd.snd = intentClosure r Set.univ
@[simp]
theorem
Concept.bot_fst
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
⊥.toProd.fst = extentClosure r Set.univ
@[simp]
theorem
Concept.supₛ_fst
{α : Type u_2}
{β : Type u_1}
{r : α → β → Prop}
(S : Set (Concept α β r))
:
(supₛ S).toProd.fst = extentClosure r (Set.interᵢ fun c => Set.interᵢ fun h => c.toProd.snd)
@[simp]
theorem
Concept.supₛ_snd
{α : Type u_2}
{β : Type u_1}
{r : α → β → Prop}
(S : Set (Concept α β r))
:
(supₛ S).toProd.snd = Set.interᵢ fun c => Set.interᵢ fun h => c.toProd.snd
@[simp]
theorem
Concept.infₛ_fst
{α : Type u_2}
{β : Type u_1}
{r : α → β → Prop}
(S : Set (Concept α β r))
:
(infₛ S).toProd.fst = Set.interᵢ fun c => Set.interᵢ fun h => c.toProd.fst
@[simp]
theorem
Concept.infₛ_snd
{α : Type u_2}
{β : Type u_1}
{r : α → β → Prop}
(S : Set (Concept α β r))
:
(infₛ S).toProd.snd = intentClosure r (Set.interᵢ fun c => Set.interᵢ fun h => c.toProd.fst)
@[simp]
theorem
Concept.swap_toProd
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
(c : Concept α β r)
:
(Concept.swap c).toProd = Prod.swap c.toProd
def
Concept.swap
{α : Type u_1}
{β : Type u_2}
{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 := (_ : extentClosure r c.toProd.snd = c.toProd.fst), closure_snd := (_ : intentClosure r c.toProd.fst = c.toProd.snd) }
@[simp]
theorem
Concept.swap_swap
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
(c : Concept α β r)
:
Concept.swap (Concept.swap c) = c
@[simp]
theorem
Concept.swap_le_swap_iff
{α : Type u_1}
{β : Type u_2}
{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_1}
{β : Type u_2}
{r : α → β → Prop}
{c : Concept α β r}
{d : Concept α β r}
:
Concept.swap c < Concept.swap d ↔ d < c
@[simp]
theorem
Concept.swapEquiv_apply
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
∀ (a : (Concept α β r)ᵒᵈ),
↑(RelIso.toRelEmbedding Concept.swapEquiv).toEmbedding a = (Concept.swap ∘ ↑OrderDual.ofDual) a
@[simp]
theorem
Concept.swapEquiv_symm_apply
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
:
∀ (a : Concept β α (Function.swap r)),
↑(RelIso.toRelEmbedding (RelIso.symm Concept.swapEquiv)).toEmbedding a = (↑OrderDual.toDual ∘ Concept.swap) a