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 #

Davey, Priestley Introduction to Lattices and Order

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

intent_closure r s = {b : β | ∀ ⦃a : α⦄, a ∈ s → r 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

extent_closure r t = {a : α | ∀ ⦃b : β⦄, b ∈ t → r a b}

theorem subset_intent_closure_iff_subset_extent_closure {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : set α} {t : set β} :

t ⊆ intent_closure r s ↔ s ⊆ extent_closure r t

theorem gc_intent_closure_extent_closure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) :

galois_connection (⇑order_dual.to_dual ∘ intent_closure r) (extent_closure r ∘ ⇑order_dual.of_dual)

theorem intent_closure_swap {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : set β) :

intent_closure (function.swap r) t = extent_closure r t

theorem extent_closure_swap {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : set α) :

extent_closure (function.swap r) s = intent_closure r s

@[simp]

theorem intent_closure_empty {α : Type u_2} {β : Type u_3} (r : α → β → Prop) :

intent_closure r ∅ = set.univ

@[simp]

theorem extent_closure_empty {α : Type u_2} {β : Type u_3} (r : α → β → Prop) :

extent_closure r ∅ = set.univ

@[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 α) :

s ⊆ extent_closure r (intent_closure r s)

theorem subset_intent_closure_extent_closure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : set β) :

t ⊆ intent_closure r (extent_closure r t)

@[simp]

theorem intent_closure_extent_closure_intent_closure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : set α) :

intent_closure r (extent_closure r (intent_closure r s)) = intent_closure r s

@[simp]

theorem extent_closure_intent_closure_extent_closure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : set β) :

extent_closure r (intent_closure r (extent_closure r t)) = extent_closure r t

theorem intent_closure_anti {α : Type u_2} {β : Type u_3} (r : α → β → Prop) :

antitone (intent_closure r)

theorem extent_closure_anti {α : Type u_2} {β : Type u_3} (r : α → β → Prop) :

antitone (extent_closure r)

Concepts #

structure concept (α : Type u_2) (β : Type u_3) (r : α → β → Prop) :

Type (max u_2 u_3)

to_prod : set α × set β
closure_fst : intent_closure r self.to_prod.fst = self.to_prod.snd
closure_snd : extent_closure r self.to_prod.snd = self.to_prod.fst

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

concept.has_sup = {sup := λ (c d : concept α β r), {to_prod := (extent_closure r (c.to_prod.snd ∩ d.to_prod.snd), c.to_prod.snd ∩ d.to_prod.snd), closure_fst := _, closure_snd := _}}

@[protected, instance]

def concept.has_inf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

has_inf (concept α β r)

Equations

concept.has_inf = {inf := λ (c d : concept α β r), {to_prod := (c.to_prod.fst ∩ d.to_prod.fst, intent_closure r (c.to_prod.fst ∩ d.to_prod.fst)), closure_fst := _, closure_snd := _}}

@[protected, instance]

def concept.semilattice_inf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

semilattice_inf (concept α β r)

Equations

concept.semilattice_inf = function.injective.semilattice_inf (λ (c : concept α β r), c.to_prod.fst) concept.fst_injective concept.semilattice_inf._proof_1

@[simp]

theorem concept.fst_subset_fst_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : concept α β r} :

c.to_prod.fst ⊆ d.to_prod.fst ↔ c ≤ d

@[simp]

theorem concept.fst_ssubset_fst_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : concept α β r} :

c.to_prod.fst ⊂ d.to_prod.fst ↔ c < d

@[simp]

theorem concept.snd_subset_snd_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : concept α β r} :

c.to_prod.snd ⊆ d.to_prod.snd ↔ d ≤ c

@[simp]

theorem concept.snd_ssubset_snd_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : concept α β r} :

c.to_prod.snd ⊂ d.to_prod.snd ↔ d < c

theorem concept.strict_mono_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

strict_mono (prod.fst ∘ concept.to_prod)

theorem concept.strict_anti_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

strict_anti (prod.snd ∘ concept.to_prod)

@[protected, instance]

def concept.lattice {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

lattice (concept α β r)

Equations

concept.lattice = {sup := has_sup.sup concept.has_sup, le := semilattice_inf.le concept.semilattice_inf, lt := semilattice_inf.lt concept.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf concept.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

@[protected, instance]

def concept.bounded_order {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

bounded_order (concept α β r)

Equations

concept.bounded_order = {top := {to_prod := (set.univ α, intent_closure r set.univ), closure_fst := _, closure_snd := _}, le_top := _, bot := {to_prod := (extent_closure r set.univ, set.univ β), closure_fst := _, closure_snd := _}, bot_le := _}

@[protected, instance]

def concept.has_Sup {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

has_Sup (concept α β r)

Equations

concept.has_Sup = {Sup := λ (S : set (concept α β r)), {to_prod := (extent_closure r (⋂ (c : concept α β r) (H : c ∈ S), c.to_prod.snd), ⋂ (c : concept α β r) (H : c ∈ S), c.to_prod.snd), closure_fst := _, closure_snd := _}}

@[protected, instance]

def concept.has_Inf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

has_Inf (concept α β r)

Equations

concept.has_Inf = {Inf := λ (S : set (concept α β r)), {to_prod := (⋂ (c : concept α β r) (H : c ∈ S), c.to_prod.fst, intent_closure r (⋂ (c : concept α β r) (H : c ∈ S), c.to_prod.fst)), closure_fst := _, closure_snd := _}}

@[protected, instance]

def concept.complete_lattice {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

complete_lattice (concept α β r)

Equations

concept.complete_lattice = {sup := lattice.sup concept.lattice, le := lattice.le concept.lattice, lt := lattice.lt concept.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf concept.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup concept.has_Sup, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf concept.has_Inf, Inf_le := _, le_Inf := _, top := bounded_order.top concept.bounded_order, bot := bounded_order.bot concept.bounded_order, le_top := _, bot_le := _}

@[simp]

theorem concept.top_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

⊤.to_prod.fst = set.univ

@[simp]

theorem concept.top_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

⊤.to_prod.snd = intent_closure r set.univ

@[simp]

theorem concept.bot_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

⊥.to_prod.fst = extent_closure r set.univ

@[simp]

theorem concept.bot_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

⊥.to_prod.snd = set.univ

@[simp]

theorem concept.sup_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : concept α β r) :

(c ⊔ d).to_prod.fst = extent_closure r (c.to_prod.snd ∩ d.to_prod.snd)

@[simp]

theorem concept.sup_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : concept α β r) :

(c ⊔ d).to_prod.snd = c.to_prod.snd ∩ d.to_prod.snd

@[simp]

theorem concept.inf_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : concept α β r) :

(c ⊓ d).to_prod.fst = c.to_prod.fst ∩ d.to_prod.fst

@[simp]

theorem concept.inf_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : concept α β r) :

(c ⊓ d).to_prod.snd = intent_closure r (c.to_prod.fst ∩ d.to_prod.fst)

@[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

concept.inhabited = {default := ⊥}

def concept.swap {α : Type u_2} {β : Type u_3} {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

c.swap = {to_prod := c.to_prod.swap, closure_fst := _, closure_snd := _}

@[simp]

theorem concept.swap_to_prod {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : concept α β r) :

c.swap.to_prod = c.to_prod.swap

@[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)ᵒᵈ) :

⇑concept.swap_equiv ᾰ = (concept.swap ∘ ⇑order_dual.of_dual) ᾰ

def concept.swap_equiv {α : Type u_2} {β : Type u_3} {r : α → β → Prop} :

(concept α β r)ᵒᵈ ≃o concept β α (function.swap r)

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

Equations

concept.swap_equiv = {to_equiv := {to_fun := concept.swap ∘ ⇑order_dual.of_dual, inv_fun := ⇑order_dual.to_dual ∘ concept.swap, left_inv := _, right_inv := _}, map_rel_iff' := _}

@[simp]

theorem concept.swap_equiv_symm_apply {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (ᾰ : concept β α (function.swap r)) :

⇑(rel_iso.symm concept.swap_equiv) ᾰ = (⇑order_dual.to_dual ∘ concept.swap) ᾰ