Mathlib Map

Theorems · Definition · order theory

Concept.extent

{α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → Concept α β r → Set α

The extent of a concept.

Defined in
Mathlib.Order.Concept
Cited by
52 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

DedekindCut.left · cited by 16DedekindCut.leftConcept.upperPolar_extent · cited by 9Concept.upperPolar_extentConcept.lowerPolar_intent · cited by 8Concept.lowerPolar_intentConcept.swap · cited by 7Concept.swapConcept.intent_subset_intent_iff · cited by 5Concept.intent_subset_int…Concept.rel_extent_intent · cited by 5Concept.rel_extent_intentConcept.ext · cited by 5Concept.extConcept.mem_extent_of_rel_extent · cited by 4Concept.mem_extent_of_rel…Concept.copy · cited by 4Concept.copyConcept.mem_intent_of_intent_rel · cited by 3Concept.mem_intent_of_int…Concept.extent_ssubset_extent_iff · cited by 2Concept.extent_ssubset_ex…Concept.extent_subset_extent_iff · cited by 2Concept.extent_subset_ext…Concept.isCompl_extent_intent · cited by 2Concept.isCompl_extent_in…Concept.isExtent_extent · cited by 2Concept.isExtent_extentConcept.extent_injective · cited by 2Concept.extent_injectiveSet · cited by 53352SetConcept · cited by 78ConceptConcept.extentCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • Conceptstatement and proof · cited by 78

Cited by55

Results whose statement or proof uses this declaration.