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

• Davey, Priestley Introduction to Lattices and Order
• Birkhoff, Garrett Lattice Theory

Tags

concept, formal concept analysis, intent, extend, 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}

@[deprecated upperPolar (since := "2025-07-10")]

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

Alias of upperPolar.

---

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

• @intentClosure = @upperPolar

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}

@[deprecated lowerPolar (since := "2025-07-10")]

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

Alias of lowerPolar.

---

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

• @extentClosure = @lowerPolar

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

@[deprecated subset_upperPolar_iff_subset_lowerPolar (since := "2025-07-10")]

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

Alias of subset_upperPolar_iff_subset_lowerPolar.

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

@[deprecated gc_upperPolar_lowerPolar (since := "2025-07-10")]

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

Alias of gc_upperPolar_lowerPolar.

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

@[deprecated upperPolar_swap (since := "2025-07-10")]

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

Alias of upperPolar_swap.

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

@[deprecated lowerPolar_swap (since := "2025-07-10")]

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

Alias of lowerPolar_swap.

@[simp]

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

@[deprecated upperPolar_empty (since := "2025-07-10")]

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

Alias of upperPolar_empty.

@[simp]

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

@[deprecated lowerPolar_empty (since := "2025-07-10")]

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

Alias of lowerPolar_empty.

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

@[deprecated upperPolar_union (since := "2025-07-10")]

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

Alias of upperPolar_union.

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

@[deprecated lowerPolar_union (since := "2025-07-10")]

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

Alias of lowerPolar_union.

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

@[deprecated upperPolar_iUnion (since := "2025-07-10")]

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

Alias of upperPolar_iUnion.

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

@[deprecated lowerPolar_iUnion (since := "2025-07-10")]

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

Alias of lowerPolar_iUnion.

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

@[deprecated upperPolar_iUnion₂ (since := "2025-07-10")]

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

Alias of upperPolar_iUnion₂.

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

@[deprecated lowerPolar_iUnion₂ (since := "2025-07-10")]

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

Alias of lowerPolar_iUnion₂.

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

@[deprecated subset_lowerPolar_upperPolar (since := "2025-07-10")]

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

Alias of subset_lowerPolar_upperPolar.

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

@[deprecated subset_upperPolar_lowerPolar (since := "2025-07-10")]

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

Alias of subset_upperPolar_lowerPolar.

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

@[deprecated upperPolar_lowerPolar_upperPolar (since := "2025-07-10")]

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

Alias of upperPolar_lowerPolar_upperPolar.

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

@[deprecated lowerPolar_upperPolar_lowerPolar (since := "2025-07-10")]

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

Alias of lowerPolar_upperPolar_lowerPolar.

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

@[deprecated upperPolar_anti (since := "2025-07-10")]

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

Alias of upperPolar_anti.

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

@[deprecated lowerPolar_anti (since := "2025-07-10")]

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

Alias of lowerPolar_anti.

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.

@[deprecated Concept.extent (since := "2025-07-10")]

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

Alias of Concept.extent.

---

The extent of a concept.

Equations

• @Concept.fst = @Concept.extent

@[deprecated Concept.intent (since := "2025-07-10")]

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

Alias of Concept.intent.

---

The intent of a concept.

Equations

• @Concept.snd = @Concept.intent

@[deprecated Concept.upperPolar_extent (since := "2025-07-10")]

theorem Concept.closure_fst {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (self : Concept α β r) : upperPolar r self.extent = self.intent

Alias of Concept.upperPolar_extent.

---

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

@[deprecated Concept.lowerPolar_intent (since := "2025-07-10")]

theorem Concept.closure_snd {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (self : Concept α β r) : lowerPolar r self.intent = self.extent

Alias of Concept.lowerPolar_intent.

---

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

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

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

@[deprecated Concept.extent_injective (since := "2025-07-10")]

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

Alias of Concept.extent_injective.

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

@[deprecated Concept.intent_injective (since := "2025-07-10")]

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

Alias of Concept.intent_injective.

instance Concept.instSupConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Max (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} : Min (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} : SemilatticeInf (Concept α β r)

Equations

• Concept.instSemilatticeInfConcept = Function.Injective.semilatticeInf Concept.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

@[deprecated Concept.extent_subset_extent_iff (since := "2025-07-10")]

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

Alias of Concept.extent_subset_extent_iff.

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

@[deprecated Concept.extent_ssubset_extent_iff (since := "2025-07-10")]

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

Alias of Concept.extent_ssubset_extent_iff.

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

@[deprecated Concept.intent_subset_intent_iff (since := "2025-07-10")]

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

Alias of Concept.intent_subset_intent_iff.

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

@[deprecated Concept.intent_ssubset_intent_iff (since := "2025-07-10")]

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

Alias of Concept.intent_ssubset_intent_iff.

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

@[deprecated Concept.strictMono_extent (since := "2025-07-10")]

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

Alias of Concept.strictMono_extent.

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

@[deprecated Concept.strictAnti_intent (since := "2025-07-10")]

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

Alias of Concept.strictAnti_intent.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[deprecated Concept.extent_top (since := "2025-07-10")]

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

Alias of Concept.extent_top.

@[simp]

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

@[deprecated Concept.intent_top (since := "2025-07-10")]

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

Alias of Concept.intent_top.

@[simp]

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

@[deprecated Concept.extent_bot (since := "2025-07-10")]

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

Alias of Concept.extent_bot.

@[simp]

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

@[deprecated Concept.intent_bot (since := "2025-07-10")]

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

Alias of Concept.intent_bot.

@[simp]

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)

@[deprecated Concept.extent_top (since := "2025-07-10")]

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

Alias of Concept.extent_top.

@[simp]

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

@[deprecated Concept.intent_sup (since := "2025-07-10")]

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

Alias of Concept.intent_sup.

@[simp]

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

@[deprecated Concept.extent_inf (since := "2025-07-10")]

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

Alias of Concept.extent_inf.

@[simp]

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)

@[deprecated Concept.intent_inf (since := "2025-07-10")]

theorem Concept.inf_snd {α : 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_inf.

@[simp]

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

@[deprecated Concept.extent_sSup (since := "2025-07-10")]

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

Alias of Concept.extent_sSup.

@[simp]

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

@[deprecated Concept.intent_sSup (since := "2025-07-10")]

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

Alias of Concept.intent_sSup.

@[simp]

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

@[deprecated Concept.extent_sInf (since := "2025-07-10")]

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

Alias of Concept.extent_sInf.

@[simp]

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

@[deprecated Concept.intent_sInf (since := "2025-07-10")]

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

Alias of Concept.intent_sInf.

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.swap_extent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : c.swap.extent = c.intent

@[simp]

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

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