Theorems · Inductive type · order theory
Concept
(α : Type u_2) → (β : Type u_3) → (α → β → 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.
- Defined in
- Mathlib.Order.Concept
- Cited by
- 78 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by96
Results whose statement or proof uses this declaration.
- Concept.extentstatement and proof · cited by 52
- Concept.intentstatement and proof · cited by 51
- DedekindCutproof · cited by 27
- Concept.ofAttributesstatement · cited by 9
- Concept.ofObjectsstatement · cited by 9
- Concept.upperPolar_extentstatement and proof · cited by 9
- Concept.lowerPolar_intentstatement and proof · cited by 8
- Concept.swapstatement and proof · cited by 7
- Concept.intent_subset_intent_iffstatement and proof · cited by 5
- Concept.rel_extent_intentstatement and proof · cited by 5
- Concept.extstatement and proof · cited by 5
- Concept.mem_extent_of_rel_extentstatement and proof · cited by 4