mathlib3 documentation

order.concept

Formal concept analysis #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 intent_closure {α : 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
def extent_closure {α : 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
theorem subset_intent_closure_iff_subset_extent_closure {α : Type u_2} {β : Type u_3} {r : α β Prop} {s : set α} {t : set β} :
theorem intent_closure_swap {α : Type u_2} {β : Type u_3} (r : α β Prop) (t : set β) :
theorem extent_closure_swap {α : Type u_2} {β : Type u_3} (r : α β Prop) (s : set α) :
@[simp]
theorem intent_closure_empty {α : Type u_2} {β : Type u_3} (r : α β Prop) :
@[simp]
theorem extent_closure_empty {α : Type u_2} {β : Type u_3} (r : α β Prop) :
@[simp]
theorem intent_closure_union {α : Type u_2} {β : Type u_3} (r : α β Prop) (s₁ s₂ : set α) :
intent_closure r (s₁ s₂) = intent_closure r s₁ intent_closure r s₂
@[simp]
theorem extent_closure_union {α : Type u_2} {β : Type u_3} (r : α β Prop) (t₁ t₂ : set β) :
extent_closure r (t₁ t₂) = extent_closure r t₁ extent_closure r t₂
@[simp]
theorem intent_closure_Union {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α β Prop) (f : ι set α) :
intent_closure r ( (i : ι), f i) = (i : ι), intent_closure r (f i)
@[simp]
theorem extent_closure_Union {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α β Prop) (f : ι set β) :
extent_closure r ( (i : ι), f i) = (i : ι), extent_closure r (f i)
@[simp]
theorem intent_closure_Union₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι Sort u_5} (r : α β Prop) (f : Π (i : ι), κ i set α) :
intent_closure r ( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), intent_closure r (f i j)
@[simp]
theorem extent_closure_Union₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι Sort u_5} (r : α β Prop) (f : Π (i : ι), κ i set β) :
extent_closure r ( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), extent_closure r (f i j)
theorem subset_extent_closure_intent_closure {α : Type u_2} {β : Type u_3} (r : α β Prop) (s : set α) :
theorem subset_intent_closure_extent_closure {α : Type u_2} {β : Type u_3} (r : α β Prop) (t : set β) :
@[simp]
theorem intent_closure_extent_closure_intent_closure {α : Type u_2} {β : Type u_3} (r : α β Prop) (s : set α) :
@[simp]
theorem extent_closure_intent_closure_extent_closure {α : Type u_2} {β : Type u_3} (r : α β Prop) (t : set β) :
theorem intent_closure_anti {α : Type u_2} {β : Type u_3} (r : α β Prop) :
theorem extent_closure_anti {α : Type u_2} {β : Type u_3} (r : α β Prop) :

Concepts #

structure concept (α : Type u_2) (β : Type u_3) (r : α β Prop) :
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.

Instances for concept
@[ext]
theorem concept.ext {α : Type u_2} {β : Type u_3} {r : α β Prop} {c d : concept α β r} (h : c.to_prod.fst = d.to_prod.fst) :
c = d
theorem concept.ext' {α : Type u_2} {β : Type u_3} {r : α β Prop} {c d : concept α β r} (h : c.to_prod.snd = d.to_prod.snd) :
c = d
theorem concept.fst_injective {α : Type u_2} {β : Type u_3} {r : α β Prop} :
function.injective (λ (c : concept α β r), c.to_prod.fst)
theorem concept.snd_injective {α : Type u_2} {β : Type u_3} {r : α β Prop} :
function.injective (λ (c : concept α β r), c.to_prod.snd)
@[protected, instance]
def concept.has_sup {α : Type u_2} {β : Type u_3} {r : α β Prop} :
has_sup (concept α β r)
Equations
@[protected, instance]
def concept.has_inf {α : Type u_2} {β : Type u_3} {r : α β Prop} :
has_inf (concept α β r)
Equations
@[protected, instance]
def concept.semilattice_inf {α : 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 d : concept α β r} :
@[simp]
theorem concept.fst_ssubset_fst_iff {α : Type u_2} {β : Type u_3} {r : α β Prop} {c d : concept α β r} :
@[simp]
theorem concept.snd_subset_snd_iff {α : Type u_2} {β : Type u_3} {r : α β Prop} {c d : concept α β r} :
@[simp]
theorem concept.snd_ssubset_snd_iff {α : Type u_2} {β : Type u_3} {r : α β Prop} {c d : concept α β r} :
theorem concept.strict_mono_fst {α : Type u_2} {β : Type u_3} {r : α β Prop} :
theorem concept.strict_anti_snd {α : Type u_2} {β : Type u_3} {r : α β Prop} :
@[protected, instance]
def concept.bounded_order {α : Type u_2} {β : Type u_3} {r : α β Prop} :
Equations
@[protected, instance]
def concept.has_Sup {α : Type u_2} {β : Type u_3} {r : α β Prop} :
has_Sup (concept α β r)
Equations
@[protected, instance]
def concept.has_Inf {α : Type u_2} {β : Type u_3} {r : α β Prop} :
has_Inf (concept α β r)
Equations
@[simp]
theorem concept.top_fst {α : Type u_2} {β : Type u_3} {r : α β Prop} :
@[simp]
theorem concept.top_snd {α : Type u_2} {β : Type u_3} {r : α β Prop} :
@[simp]
theorem concept.bot_fst {α : Type u_2} {β : Type u_3} {r : α β Prop} :
@[simp]
theorem concept.bot_snd {α : Type u_2} {β : Type u_3} {r : α β Prop} :
@[simp]
theorem concept.sup_fst {α : Type u_2} {β : Type u_3} {r : α β Prop} (c d : concept α β r) :
@[simp]
theorem concept.sup_snd {α : Type u_2} {β : Type u_3} {r : α β Prop} (c d : concept α β r) :
@[simp]
theorem concept.inf_fst {α : Type u_2} {β : Type u_3} {r : α β Prop} (c d : concept α β r) :
@[simp]
theorem concept.inf_snd {α : Type u_2} {β : Type u_3} {r : α β Prop} (c d : concept α β r) :
@[simp]
theorem concept.Sup_fst {α : Type u_2} {β : Type u_3} {r : α β Prop} (S : set (concept α β r)) :
(has_Sup.Sup S).to_prod.fst = extent_closure r ( (c : concept α β r) (H : c S), c.to_prod.snd)
@[simp]
theorem concept.Sup_snd {α : Type u_2} {β : Type u_3} {r : α β Prop} (S : set (concept α β r)) :
(has_Sup.Sup S).to_prod.snd = (c : concept α β r) (H : c S), c.to_prod.snd
@[simp]
theorem concept.Inf_fst {α : Type u_2} {β : Type u_3} {r : α β Prop} (S : set (concept α β r)) :
(has_Inf.Inf S).to_prod.fst = (c : concept α β r) (H : c S), c.to_prod.fst
@[simp]
theorem concept.Inf_snd {α : Type u_2} {β : Type u_3} {r : α β Prop} (S : set (concept α β r)) :
(has_Inf.Inf S).to_prod.snd = intent_closure r ( (c : concept α β r) (H : c S), c.to_prod.fst)
@[protected, instance]
def concept.inhabited {α : Type u_2} {β : Type u_3} {r : α β Prop} :
inhabited (concept α β r)
Equations
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
@[simp]
theorem concept.swap_to_prod {α : Type u_2} {β : Type u_3} {r : α β Prop} (c : concept α β r) :
@[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 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 d : concept α β r} :
c.swap < d.swap d < c
@[simp]
theorem concept.swap_equiv_apply {α : Type u_2} {β : Type u_3} {r : α β Prop} (ᾰ : (concept α β r)ᵒᵈ) :
def concept.swap_equiv {α : 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
@[simp]
theorem concept.swap_equiv_symm_apply {α : Type u_2} {β : Type u_3} {r : α β Prop} (ᾰ : concept β α (function.swap r)) :