Documentation

Mathlib.Order.Concept

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 #

Tags #

concept, formal concept analysis, intent, extend, attribute

Intent and extent #

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

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
def extentClosure {α : Type u_1} {β : Type u_2} (r : αβProp) (t : Set β) :
Set α

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
theorem subset_intentClosure_iff_subset_extentClosure {α : Type u_2} {β : Type u_1} {r : αβProp} {s : Set α} {t : Set β} :
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 β) :
theorem extentClosure_swap {α : Type u_1} {β : Type u_2} (r : αβProp) (s : Set α) :
@[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 : ι) → κ iSet α) :
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 : ι) → κ iSet β) :
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 α) :
theorem subset_intentClosure_extentClosure {α : Type u_2} {β : Type u_1} (r : αβProp) (t : Set β) :
@[simp]
theorem intentClosure_extentClosure_intentClosure {α : Type u_1} {β : Type u_2} (r : αβProp) (s : Set α) :
@[simp]
theorem extentClosure_intentClosure_extentClosure {α : Type u_2} {β : Type u_1} (r : αβProp) (t : Set β) :
theorem intentClosure_anti {α : Type u_1} {β : Type u_2} (r : αβProp) :
theorem extentClosure_anti {α : Type u_2} {β : Type u_1} (r : αβProp) :

Concepts #

structure Concept (α : Type u_1) (β : Type u_2) (r : αβProp) extends Prod :
Type (maxu_1u_2)
  • The axiom of a Concept stating that the closure of the first set is the second set.

    closure_fst : intentClosure r toProd.fst = toProd.snd
  • The axiom of a Concept stating 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.ext {α : Type u_1} {β : Type u_2} {r : αβProp} {c : Concept α β r} {d : Concept α β r} (h : c.toProd.fst = d.toProd.fst) :
    c = d
    theorem Concept.ext' {α : Type u_2} {β : Type u_1} {r : αβProp} {c : Concept α β r} {d : Concept α β r} (h : c.toProd.snd = d.toProd.snd) :
    c = d
    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.instSupConcept {α : Type u_1} {β : Type u_2} {r : αβProp} :
    Sup (Concept α β r)
    Equations
    • One or more equations did not get rendered due to their size.
    instance Concept.instInfConcept {α : Type u_1} {β : Type u_2} {r : αβProp} :
    Inf (Concept α β r)
    Equations
    • One or more equations did not get rendered due to their size.
    instance Concept.instSemilatticeInfConcept {α : Type u_1} {β : Type u_2} {r : αβProp} :
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Concept.fst_subset_fst_iff {α : Type u_1} {β : Type u_2} {r : αβProp} {c : Concept α β r} {d : Concept α β r} :
    c.toProd.fst d.toProd.fst c d
    @[simp]
    theorem Concept.fst_ssubset_fst_iff {α : Type u_1} {β : Type u_2} {r : αβProp} {c : Concept α β r} {d : Concept α β r} :
    c.toProd.fst d.toProd.fst c < d
    @[simp]
    theorem Concept.snd_subset_snd_iff {α : Type u_2} {β : Type u_1} {r : αβProp} {c : Concept α β r} {d : Concept α β r} :
    c.toProd.snd d.toProd.snd d c
    @[simp]
    theorem Concept.snd_ssubset_snd_iff {α : Type u_2} {β : Type u_1} {r : αβProp} {c : Concept α β r} {d : Concept α β r} :
    c.toProd.snd d.toProd.snd d < c
    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.instLatticeConcept {α : Type u_1} {β : Type u_2} {r : αβProp} :
    Lattice (Concept α β r)
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • Concept.instBoundedOrderConceptToLEToPreorderToPartialOrderInstSemilatticeInfConcept = BoundedOrder.mk
    instance Concept.instSupSetConcept {α : Type u_1} {β : Type u_2} {r : αβProp} :
    SupSet (Concept α β r)
    Equations
    • One or more equations did not get rendered due to their size.
    instance Concept.instInfSetConcept {α : Type u_1} {β : Type u_2} {r : αβProp} :
    InfSet (Concept α β r)
    Equations
    • One or more equations did not get rendered due to their size.
    instance Concept.instCompleteLatticeConcept {α : Type u_1} {β : Type u_2} {r : αβProp} :
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Concept.top_fst {α : Type u_1} {β : Type u_2} {r : αβProp} :
    .toProd.fst = Set.univ
    @[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.bot_snd {α : Type u_2} {β : Type u_1} {r : αβProp} :
    .toProd.snd = Set.univ
    @[simp]
    theorem Concept.sup_fst {α : Type u_1} {β : Type u_2} {r : αβProp} (c : Concept α β r) (d : Concept α β r) :
    (c d).toProd.fst = extentClosure r (c.toProd.snd d.toProd.snd)
    @[simp]
    theorem Concept.sup_snd {α : Type u_1} {β : Type u_2} {r : αβProp} (c : Concept α β r) (d : Concept α β r) :
    (c d).toProd.snd = c.toProd.snd d.toProd.snd
    @[simp]
    theorem Concept.inf_fst {α : Type u_1} {β : Type u_2} {r : αβProp} (c : Concept α β r) (d : Concept α β r) :
    (c d).toProd.fst = c.toProd.fst d.toProd.fst
    @[simp]
    theorem Concept.inf_snd {α : Type u_1} {β : Type u_2} {r : αβProp} (c : Concept α β r) (d : Concept α β r) :
    (c d).toProd.snd = intentClosure r (c.toProd.fst d.toProd.fst)
    @[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)
    instance Concept.instInhabitedConcept {α : Type u_1} {β : Type u_2} {r : αβProp} :
    Inhabited (Concept α β r)
    Equations
    • Concept.instInhabitedConcept = { default := }
    @[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) :

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

    Equations
    @[simp]
    theorem Concept.swap_swap {α : Type u_1} {β : Type u_2} {r : αβProp} (c : Concept α β r) :
    @[simp]
    theorem Concept.swap_le_swap_iff {α : Type u_1} {β : Type u_2} {r : αβProp} {c : Concept α β r} {d : Concept α β r} :
    @[simp]
    theorem Concept.swap_lt_swap_iff {α : Type u_1} {β : Type u_2} {r : αβProp} {c : Concept α β r} {d : Concept α β r} :
    @[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
    def Concept.swapEquiv {α : Type u_1} {β : Type u_2} {r : αβProp} :

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

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