Commit 2023-01-05 21:25 cb1b0a60

View on Github →

feat: port Order.Concept (#1355) Re-submit pull#1307 as a branch of mathlib4

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Concept.lean

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.fst_ssubset_fst_iff

added theorem Concept.fst_subset_fst_iff

added theorem Concept.inf_fst

added theorem Concept.inf_snd

added theorem Concept.infₛ_fst

added theorem Concept.infₛ_snd

added theorem Concept.snd_injective

added theorem Concept.snd_ssubset_snd_iff

added theorem Concept.snd_subset_snd_iff

added theorem Concept.strict_anti_snd

added theorem Concept.strict_mono_fst

added theorem Concept.sup_fst

added theorem Concept.sup_snd

added theorem Concept.supₛ_fst

added theorem Concept.supₛ_snd

added def Concept.swap

added def Concept.swapEquiv

added theorem Concept.swap_le_swap_iff

added theorem Concept.swap_lt_swap_iff

added theorem Concept.swap_swap

added theorem Concept.top_fst

added theorem Concept.top_snd

added structure Concept

added def extentClosure

added theorem extent_closure_Union₂

added theorem extent_closure_anti

added theorem extent_closure_empty

added theorem extent_closure_intent_closure_extent_closure

added theorem extent_closure_swap

added theorem extent_closure_union

added theorem extent_closure_unionᵢ

added theorem gc_intent_closure_extent_closure

added def intentClosure

added theorem intent_closure_anti

added theorem intent_closure_empty

added theorem intent_closure_extent_closure_intent_closure

added theorem intent_closure_swap

added theorem intent_closure_union

added theorem intent_closure_unionᵢ

added theorem intent_closure_unionᵢ₂

added theorem subset_extent_closure_intent_closure

added theorem subset_intent_closure_extent_closure

added theorem subset_intent_closure_iff_subset_extent_closure