Mathlib Map

Theorems · Definition · order theory

Concept.intent

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

The intent of a concept.

Defined in
Mathlib.Order.Concept
Cited by
51 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.right · cited by 12DedekindCut.rightConcept.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.mem_extent_of_rel_extent · cited by 4Concept.mem_extent_of_rel…Concept.copy · cited by 4Concept.copyConcept.intent_ssubset_intent_iff · cited by 3Concept.intent_ssubset_in…Concept.mem_intent_of_intent_rel · cited by 3Concept.mem_intent_of_int…Concept.isCompl_extent_intent · cited by 2Concept.isCompl_extent_in…Concept.isIntent_intent · cited by 2Concept.isIntent_intentConcept.ext' · cited by 2Concept.ext'Concept.extent_sSup · cited by 1Concept.extent_sSupConcept.intent_injective · cited by 1Concept.intent_injectiveSet · cited by 53352SetConcept · cited by 78ConceptConcept.intentCITED 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 by54

Results whose statement or proof uses this declaration.