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.

## 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
• = {b : β | ∀ ⦃a : α⦄, a sr a b}
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
• = {a : α | ∀ ⦃b : β⦄, b tr a b}
theorem subset_intent_closure_iff_subset_extent_closure {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : set α} {t : set β} :
t s
theorem gc_intent_closure_extent_closure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) :
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 α) :
(s₁ s₂) = s₁ s₂
@[simp]
theorem extent_closure_union {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t₁ t₂ : set β) :
(t₁ t₂) = t₁ t₂
@[simp]
theorem intent_closure_Union {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (f : ι → set α) :
(⋃ (i : ι), f i) = ⋂ (i : ι), (f i)
@[simp]
theorem extent_closure_Union {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (f : ι → set β) :
(⋃ (i : ι), f i) = ⋂ (i : ι), (f i)
@[simp]
theorem intent_closure_Union₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} (r : α → β → Prop) (f : Π (i : ι), κ iset α) :
(⋃ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), (f i j)
@[simp]
theorem extent_closure_Union₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} (r : α → β → Prop) (f : Π (i : ι), κ iset β) :
(⋃ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), (f i j)
theorem subset_extent_closure_intent_closure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : set α) :
s s)
theorem subset_intent_closure_extent_closure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : set β) :
t t)
@[simp]
theorem intent_closure_extent_closure_intent_closure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : set α) :
s)) =
@[simp]
theorem extent_closure_intent_closure_extent_closure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : set β) :
t)) =
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 : β 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 : β 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 : β r), c.to_prod.fst)
theorem concept.snd_injective {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :
function.injective (λ (c : β 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 : β r} :
@[simp]
theorem concept.fst_ssubset_fst_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : β r} :
@[simp]
theorem concept.snd_subset_snd_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : β r} :
@[simp]
theorem concept.snd_ssubset_snd_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : β 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.lattice {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :
lattice (concept α β r)
Equations
@[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
@[protected, instance]
def concept.complete_lattice {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :
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 : β r) :
@[simp]
theorem concept.sup_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : β r) :
@[simp]
theorem concept.inf_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : β r) :
@[simp]
theorem concept.inf_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : β 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 = (⋂ (c : β 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 : β 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 : β 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 = (⋂ (c : β 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 : β 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 : β r) :
@[simp]
theorem concept.swap_swap {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : β r) :
c.swap.swap = c
@[simp]
theorem concept.swap_le_swap_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : β r} :
c.swap d.swap d c
@[simp]
theorem concept.swap_lt_swap_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : β 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} :
(concept α β r)ᵒᵈ ≃o α

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} (ᾰ : α ) :