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.

References

• [Davey, Priestley Introduction to Lattices and Order][davey_priestley]
• [Birkhoff, Garrett Lattice Theory][birkhoff1940]

Tags

concept, formal concept analysis, intent, extent, object, attribute

Lower and upper polars

def upperPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : Set β

The upper polar of s : Set α along a relation r : α → β → Prop is the set of all elements which r relates to all elements of s.

Equations

• upperPolar r s = {b : β | ∀ ⦃a : α⦄, a ∈ s → r a b}

def lowerPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : Set α

The lower polar of t : Set β along a relation r : α → β → Prop is the set of all elements which r relates to all elements of t.

Equations

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

@[simp]

theorem upperPolar_le {α : Type u_2} {s : Set α} [LE α] : upperPolar (fun (x1 x2 : α) => x1 ≤ x2) s = upperBounds s

@[simp]

theorem lowerPolar_le {β : Type u_3} {t : Set β} [LE β] : lowerPolar (fun (x1 x2 : β) => x1 ≤ x2) t = lowerBounds t

theorem mem_upperPolar_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} {b : β} : b ∈ upperPolar r s ↔ ∀ ⦃a : α⦄, a ∈ s → r a b

theorem mem_lowerPolar_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} {a : α} : a ∈ lowerPolar r t ↔ ∀ ⦃b : β⦄, b ∈ t → r a b

theorem subset_upperPolar_iff_subset_lowerPolar {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} {t : Set β} : t ⊆ upperPolar r s ↔ s ⊆ lowerPolar r t

theorem gc_upperPolar_lowerPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : GaloisConnection (⇑OrderDual.toDual ∘ upperPolar r) (lowerPolar r ∘ ⇑OrderDual.ofDual)

theorem gc_lowerPolar_upperPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : GaloisConnection (⇑OrderDual.toDual ∘ lowerPolar r) (upperPolar r ∘ ⇑OrderDual.ofDual)

theorem upperPolar_swap {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : upperPolar (Function.swap r) t = lowerPolar r t

theorem lowerPolar_swap {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : lowerPolar (Function.swap r) s = upperPolar r s

@[simp]

theorem upperPolar_empty {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : upperPolar r ∅ = Set.univ

@[simp]

theorem lowerPolar_empty {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : lowerPolar r ∅ = Set.univ

@[simp]

theorem mem_upperPolar_singleton {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {a : α} {b : β} : b ∈ upperPolar r {a} ↔ r a b

@[simp]

theorem mem_lowerPolar_singleton {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {a : α} {b : β} : a ∈ lowerPolar r {b} ↔ r a b

@[simp]

theorem upperPolar_union {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s₁ s₂ : Set α) : upperPolar r (s₁ ∪ s₂) = upperPolar r s₁ ∩ upperPolar r s₂

@[simp]

theorem lowerPolar_union {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t₁ t₂ : Set β) : lowerPolar r (t₁ ∪ t₂) = lowerPolar r t₁ ∩ lowerPolar r t₂

@[simp]

theorem upperPolar_iUnion {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (f : ι → Set α) : upperPolar r (⋃ (i : ι), f i) = ⋂ (i : ι), upperPolar r (f i)

@[simp]

theorem lowerPolar_iUnion {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (f : ι → Set β) : lowerPolar r (⋃ (i : ι), f i) = ⋂ (i : ι), lowerPolar r (f i)

theorem upperPolar_iUnion₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} (r : α → β → Prop) (f : (i : ι) → κ i → Set α) : upperPolar r (⋃ (i : ι), ⋃ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), upperPolar r (f i j)

theorem lowerPolar_iUnion₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} (r : α → β → Prop) (f : (i : ι) → κ i → Set β) : lowerPolar r (⋃ (i : ι), ⋃ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), lowerPolar r (f i j)

theorem subset_lowerPolar_upperPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : s ⊆ lowerPolar r (upperPolar r s)

theorem subset_upperPolar_lowerPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : t ⊆ upperPolar r (lowerPolar r t)

@[simp]

theorem upperPolar_lowerPolar_upperPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : upperPolar r (lowerPolar r (upperPolar r s)) = upperPolar r s

@[simp]

theorem lowerPolar_upperPolar_lowerPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : lowerPolar r (upperPolar r (lowerPolar r t)) = lowerPolar r t

theorem upperPolar_anti {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : Antitone (upperPolar r)

theorem lowerPolar_anti {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : Antitone (lowerPolar r)

theorem lowerPolar_upperPolar_monotone {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : Monotone (lowerPolar r ∘ upperPolar r)

theorem upperPolar_lowerPolar_monotone {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : Monotone (upperPolar r ∘ lowerPolar r)

def extentClosure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : ClosureOperator (Set α)

The extentClosure of a set is the smallest extent containing it. See IsExtent.lowerPolar_upperPolar_subset for this proof.

Equations

• extentClosure r = ⋯.closureOperator

@[simp]

theorem extentClosure_apply {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (x : Set α) : (extentClosure r) x = lowerPolar r (upperPolar r x)

@[simp]

theorem extentClosure_isClosed {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (x : Set α) : (extentClosure r).IsClosed x = (lowerPolar r (upperPolar r x) = x)

def intentClosure {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : ClosureOperator (Set β)

The intentClosure of a set is the smallest intent containing it. See IsIntent.upperPolar_lowerPolar_subset for this proof.

Equations

• intentClosure r = ⋯.closureOperator

@[simp]

theorem intentClosure_isClosed {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (x : Set β) : (intentClosure r).IsClosed x = (upperPolar r (lowerPolar r x) = x)

@[simp]

theorem intentClosure_apply {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (x : Set β) : (intentClosure r) x = upperPolar r (lowerPolar r x)

Intent and extent

def Order.IsExtent {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : Prop

A set is an extent when either of the following equivalent definitions holds:

• The lowerPolar of its upperPolar is itself.
• The set is the lowerPolar of some other set.

The latter is used as a definition, but one can rewrite using the former via IsExtent.eq.

Equations

• Order.IsExtent r s = (s ∈ Set.range (lowerPolar r))

@[simp]

theorem Order.isExtent_lowerPolar {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} : IsExtent r (lowerPolar r t)

theorem Order.isExtent_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} : IsExtent r s ↔ lowerPolar r (upperPolar r s) = s

theorem Order.IsExtent.eq {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} : IsExtent r s → lowerPolar r (upperPolar r s) = s

Alias of the forward direction of Order.isExtent_iff.

@[simp]

theorem Order.IsExtent.univ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : IsExtent r Set.univ

theorem Order.IsExtent.inter {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s s' : Set α} : IsExtent r s → IsExtent r s' → IsExtent r (s ∩ s')

theorem Order.IsExtent.iInter {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Set α) (hf : ∀ (i : ι), IsExtent r (f i)) : IsExtent r (⋂ (i : ι), f i)

theorem Order.IsExtent.iInter₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} {r : α → β → Prop} (f : (i : ι) → κ i → Set α) (hf : ∀ (i : ι) (j : κ i), IsExtent r (f i j)) : IsExtent r (⋂ (i : ι), ⋂ (j : κ i), f i j)

theorem Order.IsExtent.lowerPolar_upperPolar_subset {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s s' : Set α} (h : IsExtent r s) (hs' : s' ⊆ s) : lowerPolar r (upperPolar r s') ⊆ s

def Order.IsIntent {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : Prop

A set is an intent when either of the following equivalent definitions holds:

• The upperPolar of its lowerPolar is itself.
• The set is the upperPolar of some other set.

The latter is used as a definition, but one can rewrite using the former via IsIntent.eq.

Equations

• Order.IsIntent r t = (t ∈ Set.range (upperPolar r))

@[simp]

theorem Order.isIntent_upperPolar {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} : IsIntent r (upperPolar r s)

theorem Order.isIntent_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} : IsIntent r t ↔ upperPolar r (lowerPolar r t) = t

theorem Order.IsIntent.eq {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} : IsIntent r t → upperPolar r (lowerPolar r t) = t

Alias of the forward direction of Order.isIntent_iff.

@[simp]

theorem Order.IsIntent.univ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : IsIntent r Set.univ

theorem Order.IsIntent.inter {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t t' : Set β} : IsIntent r t → IsIntent r t' → IsIntent r (t ∩ t')

theorem Order.IsIntent.iInter {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Set β) (hf : ∀ (i : ι), IsIntent r (f i)) : IsIntent r (⋂ (i : ι), f i)

theorem Order.IsIntent.iInter₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} {r : α → β → Prop} (f : (i : ι) → κ i → Set β) (hf : ∀ (i : ι) (j : κ i), IsIntent r (f i j)) : IsIntent r (⋂ (i : ι), ⋂ (j : κ i), f i j)

theorem Order.IsIntent.upperPolar_lowerPolar_subset {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t t' : Set β} (h : IsIntent r t) (ht' : t' ⊆ t) : upperPolar r (lowerPolar r t') ⊆ t

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.

• extent : Set α

  The extent of a concept.

• intent : Set β

  The intent of a concept.

• upperPolar_extent : upperPolar r self.extent = self.intent

  The intent consists of all elements related to all elements of the extent.

• lowerPolar_intent : lowerPolar r self.intent = self.extent

  The extent consists of all elements related to all elements of the intent.

theorem Concept.ext {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} (h : c.extent = d.extent) : c = d

See Concept.ext' for a version using the intent.

theorem Concept.ext_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c = d ↔ c.extent = d.extent

theorem Concept.ext' {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} (h : c.intent = d.intent) : c = d

See Concept.ext for a version using the extent.

theorem Concept.extent_injective {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Function.Injective extent

theorem Concept.intent_injective {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Function.Injective intent

def Concept.copy {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent) (hi : i = c.intent) : Concept α β r

Copy a concept, adjusting definitional equalities.

Equations

• c.copy e i he hi = { extent := e, intent := i, upperPolar_extent := ⋯, lowerPolar_intent := ⋯ }

@[simp]

theorem Concept.intent_copy {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent) (hi : i = c.intent) : (c.copy e i he hi).intent = i

@[simp]

theorem Concept.extent_copy {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent) (hi : i = c.intent) : (c.copy e i he hi).extent = e

theorem Concept.copy_eq {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent) (hi : i = c.intent) : c.copy e i he hi = c

def Concept.ofIsExtent {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) (hs : Order.IsExtent r s) : Concept α β r

Define a concept from an extent, by setting the intent to its upper polar.

Equations

• Concept.ofIsExtent r s hs = { extent := s, intent := upperPolar r s, upperPolar_extent := ⋯, lowerPolar_intent := ⋯ }

@[simp]

theorem Concept.intent_ofIsExtent {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) (hs : Order.IsExtent r s) : (ofIsExtent r s hs).intent = upperPolar r s

@[simp]

theorem Concept.extent_ofIsExtent {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) (hs : Order.IsExtent r s) : (ofIsExtent r s hs).extent = s

@[simp]

theorem Concept.isExtent_extent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : Order.IsExtent r c.extent

theorem Concept.isExtent_iff_exists_concept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} : Order.IsExtent r s ↔ ∃ (c : Concept α β r), c.extent = s

def Concept.ofIsIntent {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) (ht : Order.IsIntent r t) : Concept α β r

Define a concept from an intent, by setting the extent to its lower polar.

Equations

• Concept.ofIsIntent r t ht = { extent := lowerPolar r t, intent := t, upperPolar_extent := ⋯, lowerPolar_intent := ⋯ }

@[simp]

theorem Concept.extent_ofIsIntent {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) (ht : Order.IsIntent r t) : (ofIsIntent r t ht).extent = lowerPolar r t

@[simp]

theorem Concept.intent_ofIsIntent {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) (ht : Order.IsIntent r t) : (ofIsIntent r t ht).intent = t

@[simp]

theorem Concept.isIntent_intent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : Order.IsIntent r c.intent

theorem Concept.isIntent_iff_exists_concept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} : Order.IsIntent r t ↔ ∃ (c : Concept α β r), c.intent = t

def Concept.ofObjects {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : Concept α β r

The concept generated from the upper polar of a set, i.e. the smallest concept containing the set of objects s.

Equations

• Concept.ofObjects r s = Concept.ofIsIntent r (upperPolar r s) ⋯

@[simp]

theorem Concept.extent_ofObjects {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : (ofObjects r s).extent = lowerPolar r (upperPolar r s)

@[simp]

theorem Concept.intent_ofObjects {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : (ofObjects r s).intent = upperPolar r s

@[reducible, inline]

abbrev Concept.ofObject {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (a : α) : Concept α β r

The concept generated by a single object.

Equations

• Concept.ofObject r a = Concept.ofObjects r {a}

@[simp]

theorem Concept.ofObjects_extent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} : ofObjects r c.extent = c

theorem Concept.extent_ofObjects_of_isExtent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} (hs : Order.IsExtent r s) : (ofObjects r s).extent = s

theorem Concept.leftInverse_ofObjects_extent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Function.LeftInverse (ofObjects r) extent

theorem Concept.leftInvOn_extent_ofObjects {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Set.LeftInvOn extent (ofObjects r) {s : Set α | Order.IsExtent r s}

theorem Concept.surjective_ofObjects {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Function.Surjective (ofObjects r)

def Concept.ofAttributes {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : Concept α β r

The concept generated from the lower polar of a set, i.e. the smallest concept whose set of attributes is contained in t.

Equations

• Concept.ofAttributes r t = Concept.ofIsExtent r (lowerPolar r t) ⋯

@[simp]

theorem Concept.intent_ofAttributes {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : (ofAttributes r t).intent = upperPolar r (lowerPolar r t)

@[simp]

theorem Concept.extent_ofAttributes {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : (ofAttributes r t).extent = lowerPolar r t

@[reducible, inline]

abbrev Concept.ofAttribute {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (b : β) : Concept α β r

The concept generated by a single attribute.

Equations

• Concept.ofAttribute r b = Concept.ofAttributes r {b}

@[simp]

theorem Concept.ofAttributes_intent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} : ofAttributes r c.intent = c

theorem Concept.intent_ofAttributes_of_isIntent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} (hs : Order.IsIntent r t) : (ofAttributes r t).intent = t

theorem Concept.leftInverse_ofAttributes_extent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Function.LeftInverse (ofAttributes r) intent

theorem Concept.leftInvOn_ofObjects_intent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Set.LeftInvOn intent (ofAttributes r) {s : Set β | Order.IsIntent r s}

theorem Concept.surjective_ofAttributes {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Function.Surjective (ofAttributes r)

theorem Concept.rel_extent_intent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {x : α} {y : β} (hx : x ∈ c.extent) (hy : y ∈ c.intent) : r x y

theorem Concept.disjoint_extent_intent {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [Std.Irrefl r'] : Disjoint c'.extent c'.intent

Note that if r' is the ≤ relation, this theorem will often not be true!

theorem Concept.mem_extent_of_rel_extent {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [IsTrans α r'] {x y : α} (hy : r' y x) (hx : x ∈ c'.extent) : y ∈ c'.extent

theorem Concept.mem_intent_of_intent_rel {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [IsTrans α r'] {x y : α} (hy : r' x y) (hx : x ∈ c'.intent) : y ∈ c'.intent

theorem Concept.codisjoint_extent_intent {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [Std.Trichotomous r'] [IsTrans α r'] : Codisjoint c'.extent c'.intent

@[implicit_reducible]

instance Concept.instPartialOrder {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : PartialOrder (Concept α β r)

Equations

• Concept.instPartialOrder = PartialOrder.lift Concept.extent ⋯

theorem Concept.isCompl_extent_intent {α : Type u_2} {r' : α → α → Prop} [IsStrictTotalOrder α r'] (c' : Concept α α r') : IsCompl c'.extent c'.intent

@[simp]

theorem Concept.compl_extent {α : Type u_2} {r' : α → α → Prop} [IsStrictTotalOrder α r'] (c' : Concept α α r') : c'.extentᶜ = c'.intent

@[simp]

theorem Concept.compl_intent {α : Type u_2} {r' : α → α → Prop} [IsStrictTotalOrder α r'] (c' : Concept α α r') : c'.intentᶜ = c'.extent

@[simp]

theorem Concept.extent_subset_extent_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.extent ⊆ d.extent ↔ c ≤ d

@[simp]

theorem Concept.extent_ssubset_extent_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.extent ⊂ d.extent ↔ c < d

@[simp]

theorem Concept.intent_subset_intent_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.intent ⊆ d.intent ↔ d ≤ c

@[simp]

theorem Concept.intent_ssubset_intent_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.intent ⊂ d.intent ↔ d < c

theorem Concept.strictMono_extent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : StrictMono extent

theorem Concept.strictAnti_intent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : StrictAnti intent

@[simp]

theorem Concept.isLowerSet_extent_le {α : Type u_6} [Preorder α] (c : Concept α α fun (x1 x2 : α) => x1 ≤ x2) : IsLowerSet c.extent

@[simp]

theorem Concept.isUpperSet_intent_le {α : Type u_6} [Preorder α] (c : Concept α α fun (x1 x2 : α) => x1 ≤ x2) : IsUpperSet c.intent

@[simp]

theorem Concept.isLowerSet_extent_lt {α : Type u_6} [PartialOrder α] (c : Concept α α fun (x1 x2 : α) => x1 < x2) : IsLowerSet c.extent

@[simp]

theorem Concept.isUpperSet_intent_lt {α : Type u_6} [PartialOrder α] (c : Concept α α fun (x1 x2 : α) => x1 < x2) : IsUpperSet c.intent

@[implicit_reducible]

instance Concept.instMax {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Max (Concept α β r)

Equations

• Concept.instMax = { max := fun (c d : Concept α β r) => Concept.ofIsIntent r (c.intent ∩ d.intent) ⋯ }

@[simp]

theorem Concept.intent_max {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊔ d).intent = c.intent ∩ d.intent

@[simp]

theorem Concept.extent_max {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊔ d).extent = lowerPolar r (c.intent ∩ d.intent)

theorem Concept.extent_sup {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊔ d).extent = lowerPolar r (c.intent ∩ d.intent)

Alias of Concept.extent_max.

theorem Concept.intent_sup {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊔ d).intent = c.intent ∩ d.intent

Alias of Concept.intent_max.

@[implicit_reducible]

instance Concept.instMin {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Min (Concept α β r)

Equations

• Concept.instMin = { min := fun (c d : Concept α β r) => Concept.ofIsExtent r (c.extent ∩ d.extent) ⋯ }

@[simp]

theorem Concept.intent_min {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊓ d).intent = upperPolar r (c.extent ∩ d.extent)

@[simp]

theorem Concept.extent_min {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊓ d).extent = c.extent ∩ d.extent

theorem Concept.extent_inf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊓ d).extent = c.extent ∩ d.extent

Alias of Concept.extent_min.

theorem Concept.intent_inf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊓ d).intent = upperPolar r (c.extent ∩ d.extent)

Alias of Concept.intent_min.

@[implicit_reducible]

instance Concept.instSemilatticeInf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : SemilatticeInf (Concept α β r)

Equations

• Concept.instSemilatticeInf = Function.Injective.semilatticeInf Concept.extent ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance Concept.instSemilatticeSup {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : SemilatticeSup (Concept α β r)

Equations

• Concept.instSemilatticeSup = Function.Injective.semilatticeSup (⇑OrderDual.toDual ∘ Concept.intent) ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance Concept.instLattice {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Lattice (Concept α β r)

Equations

• Concept.instLattice = { toSemilatticeSup := Concept.instSemilatticeSup, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[simp]

theorem Concept.ofObjects_le_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} {c : Concept α β r} : ofObjects r s ≤ c ↔ s ⊆ c.extent

theorem Concept.le_ofObjects_of_extent_subset {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} {c : Concept α β r} (h : c.extent ⊆ s) : c ≤ ofObjects r s

@[simp]

theorem Concept.le_ofAttributes_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} {c : Concept α β r} : c ≤ ofAttributes r t ↔ t ⊆ c.intent

theorem Concept.ofAttributes_le_of_intent_subset {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} {c : Concept α β r} (h : c.intent ⊆ t) : ofAttributes r t ≤ c

theorem Concept.ofObject_le_ofAttribute_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {a : α} {b : β} : ofObject r a ≤ ofAttribute r b ↔ r a b

@[implicit_reducible]

instance Concept.instBoundedOrderConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : BoundedOrder (Concept α β r)

Equations

• Concept.instBoundedOrderConcept = { top := Concept.ofIsExtent r Set.univ ⋯, le_top := ⋯, bot := Concept.ofIsIntent r Set.univ ⋯, bot_le := ⋯ }

@[simp]

theorem Concept.extent_top {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊤.extent = Set.univ

@[simp]

theorem Concept.extent_bot {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊥.extent = lowerPolar r Set.univ

@[simp]

theorem Concept.intent_top {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊤.intent = upperPolar r Set.univ

@[simp]

theorem Concept.intent_bot {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊥.intent = Set.univ

@[implicit_reducible]

instance Concept.instInfSet {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : InfSet (Concept α β r)

Equations

• Concept.instInfSet = { sInf := fun (S : Set (Concept α β r)) => Concept.ofIsExtent r (⋂ i ∈ S, i.extent) ⋯ }

@[simp]

theorem Concept.intent_sInf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sInf S).intent = upperPolar r (⋂ i ∈ S, i.extent)

@[simp]

theorem Concept.extent_sInf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sInf S).extent = ⋂ i ∈ S, i.extent

@[implicit_reducible]

instance Concept.instSupSet {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : SupSet (Concept α β r)

Equations

• Concept.instSupSet = { sSup := fun (S : Set (Concept α β r)) => Concept.ofIsIntent r (⋂ i ∈ S, i.intent) ⋯ }

@[simp]

theorem Concept.intent_sSup {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sSup S).intent = ⋂ i ∈ S, i.intent

@[simp]

theorem Concept.extent_sSup {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sSup S).extent = lowerPolar r (⋂ i ∈ S, i.intent)

@[implicit_reducible]

instance Concept.instCompleteLattice {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : CompleteLattice (Concept α β r)

One half of the fundamental theorem of concept lattices: every concept lattice is a complete lattice.

See DedekindCut.principalIso for the second half.

Equations

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

@[simp]

theorem Concept.extent_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r) : (⨆ (i : ι), f i).extent = lowerPolar r (⋂ (i : ι), (f i).intent)

@[simp]

theorem Concept.intent_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r) : (⨆ (i : ι), f i).intent = ⋂ (i : ι), (f i).intent

@[simp]

theorem Concept.extent_iInf {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r) : (⨅ (i : ι), f i).extent = ⋂ (i : ι), (f i).extent

@[simp]

theorem Concept.intent_iInf {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r) : (⨅ (i : ι), f i).intent = upperPolar r (⋂ (i : ι), (f i).extent)

@[implicit_reducible]

instance Concept.instInhabited {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Inhabited (Concept α β r)

Equations

• Concept.instInhabited = { 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 = { extent := c.intent, intent := c.extent, upperPolar_extent := ⋯, lowerPolar_intent := ⋯ }

@[simp]

theorem Concept.intent_swap {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : c.swap.intent = c.extent

@[simp]

theorem Concept.extent_swap {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : c.swap.extent = c.intent

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

def Concept.swapEquiv {α : 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.swapEquiv = { toFun := Concept.swap ∘ ⇑OrderDual.ofDual, invFun := ⇑OrderDual.toDual ∘ Concept.swap, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Concept.swapEquiv_apply {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (a✝ : (Concept α β r)ᵒᵈ) : swapEquiv a✝ = (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 swapEquiv) a✝ = (⇑OrderDual.toDual ∘ swap) a✝