Concept.snd_subset_snd_iff
theorem Concept.snd_subset_snd_iff :
∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r}, c.toProd.2 ⊆ d.toProd.2 ↔ d ≤ c := by
sorry
This theorem states that for any two concepts `c` and `d` (of types α and β respectively, related by a property `r`), the second component of the product representation of `c` is a subset of the second component of `d` if and only if `d` is less than or equal to `c`. The less than or equal to relation here is referring to the order defined on concepts, which can be different depending on the specific definition of concepts in the context.
More concisely: For concepts `c` and `d` of types `α` and `β` with a relation `r` between them, the second components of their product representations satisfy `second c ≤ second d` if and only if `d ≤ c` in the concept order.
|
intentClosure_extentClosure_intentClosure
theorem intentClosure_extentClosure_intentClosure :
∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α),
intentClosure r (extentClosure r (intentClosure r s)) = intentClosure r s
The theorem `intentClosure_extentClosure_intentClosure` states that for any relation `r` from a type `α` to a type `β`, and for any set `s` of type `α`, the intent closure of the extent closure of the intent closure of `s` under `r` is equal to the intent closure of `s` under `r`. In other words, applying the operations of extent closure and intent closure in succession on `s` under `r` doesn't change the original intent closure of `s` under `r`. This theorem provides a form of closure property for the operation of intent closure under the interplay of the relation `r` and the set `s`.
More concisely: For any relation $r$ from type $\alpha$ to type $\beta$ and set $s$ of type $\alpha$, the intent closure of the set $s$ under $r$ is equal to the intent closure of the extent closure of $s$ under $r$.
|
gc_intentClosure_extentClosure
theorem gc_intentClosure_extentClosure :
∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop),
GaloisConnection (⇑OrderDual.toDual ∘ intentClosure r) (extentClosure r ∘ ⇑OrderDual.ofDual)
This theorem states that for any relation `r` between two arbitrary types `α` and `β`, there is a Galois Connection between the intent closure of `r` and the extent closure of `r`. This connection is established through the mapping of the intent closure of `r` to the dual order using the `OrderDual.toDual` function, and the extent closure of `r` is mapped from the dual order using the `OrderDual.ofDual` function. A Galois Connection implies that the order-preserving properties between these two sets are maintained.
More concisely: For any relation `r` between types `α` and `β`, there exists a Galois Connection between the intent closure and extent closure of `r`, where the intent closure is mapped to the dual order and the extent closure is mapped from the dual order.
|
Concept.closure_fst
theorem Concept.closure_fst :
∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (self : Concept α β r),
intentClosure r self.toProd.1 = self.toProd.2
This theorem, `Concept.closure_fst`, states that for any `Concept` instance (denoted as `self`) with a relation `r : α → β → Prop`, the intent closure of the first element of the concept's product pair (`self.toProd.1`) with respect to the relation `r` is equal to the second element of the concept's product pair (`self.toProd.2`). In other words, it asserts that the set of all elements in `β` which are related to all elements in the first set of the `Concept` (as per the relation `r`) is precisely the second set of the `Concept`.
More concisely: For any `Concept` instance `self` with relation `r : α → β → Prop`, the intent closure of `self.toProd.1` with respect to `r` equals `self.toProd.2`.
|
Concept.closure_snd
theorem Concept.closure_snd :
∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (self : Concept α β r),
extentClosure r self.toProd.2 = self.toProd.1
This theorem, named `Concept.closure_snd`, states that for any `Concept` instance, the extent closure of its second set (obtained from `self.toProd.2`) with respect to a relation `r`, is equal to the first set of the `Concept` (obtained from `self.toProd.1`). In other words, the first set of the `Concept` constitutes all elements that hold the relation `r` with every element of the second set. This is a fundamental property of the `Concept` structure in this context.
More concisely: For any `Concept` instance and relation `r`, the extent closure of the second set with respect to `r` equals the first set if and only if every element in the first set is related to every element in the second set by `r`.
|