Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-22 20:22 f7905f0c

View on Github →

feat(order/concept): Concept lattices (#12286) Define concept, the type of concepts of a relation, and prove it forms a complete lattice.

Estimated changes

added theorem concept.Inf_fst
added theorem concept.Inf_snd
added theorem concept.Sup_fst
added theorem concept.Sup_snd
added theorem concept.bot_fst
added theorem concept.bot_snd
added theorem concept.ext'
added theorem concept.ext
added theorem concept.fst_injective
added theorem concept.inf_fst
added theorem concept.inf_snd
added theorem concept.snd_injective
added theorem concept.sup_fst
added theorem concept.sup_snd
added def concept.swap
added theorem concept.swap_swap
added theorem concept.top_fst
added theorem concept.top_snd
added structure concept
added def extent_closure
added theorem extent_closure_Union
added theorem extent_closure_anti
added theorem extent_closure_empty
added theorem extent_closure_swap
added theorem extent_closure_union
added def intent_closure
added theorem intent_closure_Union
added theorem intent_closure_anti
added theorem intent_closure_empty
added theorem intent_closure_swap
added theorem intent_closure_union