Documentation

Mathlib.Order.Concept

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 #

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

      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.

      Instances For
        @[simp]
        theorem Concept.closure_fst {α : Type u_2} {β : Type u_3} {r : αβProp} (self : Concept α β r) :
        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.

        @[simp]
        theorem Concept.closure_snd {α : Type u_2} {β : Type u_3} {r : αβProp} (self : Concept α β r) :
        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} :
        Equations
        @[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} :
        Equations
        • Concept.instBoundedOrderConcept = BoundedOrder.mk
        instance Concept.instSupSet {α : Type u_2} {β : Type u_3} {r : αβProp} :
        SupSet (Concept α β r)
        Equations
        • Concept.instSupSet = { sSup := fun (S : Set (Concept α β r)) => { toProd := (extentClosure r (cS, c.toProd.2), cS, c.toProd.2), closure_fst := , closure_snd := } }
        instance Concept.instInfSet {α : Type u_2} {β : Type u_3} {r : αβProp} :
        InfSet (Concept α β r)
        Equations
        • Concept.instInfSet = { sInf := fun (S : Set (Concept α β r)) => { toProd := (cS, c.toProd.1, intentClosure r (cS, c.toProd.1)), closure_fst := , closure_snd := } }
        instance Concept.instCompleteLattice {α : Type u_2} {β : Type u_3} {r : αβProp} :
        Equations
        • Concept.instCompleteLattice = 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 (cS, c.toProd.2)
        @[simp]
        theorem Concept.sSup_snd {α : Type u_2} {β : Type u_3} {r : αβProp} (S : Set (Concept α β r)) :
        (sSup S).toProd.2 = cS, c.toProd.2
        @[simp]
        theorem Concept.sInf_fst {α : Type u_2} {β : Type u_3} {r : αβProp} (S : Set (Concept α β r)) :
        (sInf S).toProd.1 = cS, 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 (cS, c.toProd.1)
        instance Concept.instInhabited {α : Type u_2} {β : Type u_3} {r : αβProp} :
        Inhabited (Concept α β r)
        Equations
        • Concept.instInhabited = { default := }
        @[simp]
        theorem Concept.swap_toProd {α : Type u_2} {β : Type u_3} {r : αβProp} (c : Concept α β r) :
        c.swap.toProd = c.swap
        def Concept.swap {α : Type u_2} {β : Type u_3} {r : αβProp} (c : Concept α β r) :

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

        Equations
        • c.swap = { toProd := c.swap, closure_fst := , closure_snd := }
        Instances For
          @[simp]
          theorem Concept.swap_swap {α : Type u_2} {β : Type u_3} {r : αβProp} (c : Concept α β r) :
          c.swap.swap = c
          @[simp]
          theorem Concept.swap_le_swap_iff {α : Type u_2} {β : Type u_3} {r : αβProp} {c : Concept α β r} {d : Concept α β r} :
          c.swap d.swap d c
          @[simp]
          theorem Concept.swap_lt_swap_iff {α : Type u_2} {β : Type u_3} {r : αβProp} {c : Concept α β r} {d : Concept α β r} :
          c.swap < d.swap d < c
          @[simp]
          theorem Concept.swapEquiv_apply {α : Type u_2} {β : Type u_3} {r : αβProp} :
          ∀ (a : (Concept α β r)ᵒᵈ), Concept.swapEquiv a = (Concept.swap OrderDual.ofDual) a
          @[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
          def Concept.swapEquiv {α : Type u_2} {β : Type u_3} {r : αβProp} :

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

          Equations
          • Concept.swapEquiv = { toFun := Concept.swap OrderDual.ofDual, invFun := OrderDual.toDual Concept.swap, left_inv := , right_inv := , map_rel_iff' := }
          Instances For