| Metric | Count |
|---|
DefinitionsCompleteLattice, compl, completeLattice, completelyDistribLattice, instBot, instCompleteLinearOrder, instInfSet, instInhabited, instLinearOrder, instMax, instMin, instPartialOrder, instSetLike, instSupSet, instTop, map, compl, completeLattice, completelyDistribLattice, instBot, instCompleteLinearOrder, instInfSet, instInhabited, instLinearOrder, instMax, instMin, instPartialOrder, instSetLike, instSupSet, instTop, map, upperSetIsoLowerSet | 32 |
Theoremscarrier_eq_coe, coe_bot, coe_compl, coe_eq_empty, coe_eq_univ, coe_iInf, coe_iInf₂, coe_iSup, coe_iSup₂, coe_inf, coe_map, coe_mk, coe_nonempty, coe_sInf, coe_sSup, coe_ssubset_coe, coe_subset_coe, coe_sup, coe_top, compl_bot, compl_compl, compl_iInf, compl_iInf₂, compl_iSup, compl_iSup₂, compl_inf, compl_le_compl, compl_map, compl_sInf, compl_sSup, compl_sup, compl_top, disjoint_coe, ext, ext_iff, instIsConcreteLE, lower, map_map, map_refl, mem_compl_iff, mem_iInf_iff, mem_iInf₂_iff, mem_iSup_iff, mem_iSup₂_iff, mem_inf_iff, mem_map, mem_mk, mem_sInf_iff, mem_sSup_iff, mem_sup_iff, mem_top, notMem_bot, symm_map, total_le, carrier_eq_coe, codisjoint_coe, coe_bot, coe_compl, coe_eq_empty, coe_eq_univ, coe_iInf, coe_iInf₂, coe_iSup, coe_iSup₂, coe_inf, coe_map, coe_mk, coe_nonempty, coe_sInf, coe_sSup, coe_ssubset_coe, coe_subset_coe, coe_sup, coe_top, compl_bot, compl_compl, compl_iInf, compl_iInf₂, compl_iSup, compl_iSup₂, compl_inf, compl_le_compl, compl_map, compl_sInf, compl_sSup, compl_sup, compl_top, ext, ext_iff, map_map, map_refl, mem_bot, mem_compl_iff, mem_iInf_iff, mem_iInf₂_iff, mem_iSup_iff, mem_iSup₂_iff, mem_inf_iff, mem_map, mem_mk, mem_sInf_iff, mem_sSup_iff, mem_sup_iff, notMem_top, symm_map, total_le, upper, upperSetIsoLowerSet_apply, upperSetIsoLowerSet_symm_apply | 109 |
| Total | 141 |
| Name | Category | Theorems |
|---|
compl 📖 | CompOp | 17 mathmath: mem_compl_iff, compl_map, compl_iInf, compl_iInf₂, compl_iSup₂, compl_inf, upperSetIsoLowerSet_symm_apply, UpperSet.compl_compl, compl_top, compl_le_compl, compl_compl, compl_iSup, coe_compl, compl_sSup, compl_sInf, compl_bot, compl_sup
|
completeLattice 📖 | CompOp | 6 mathmath: OrderEmbedding.supIrredLowerSet_apply, OrderIso.supIrredLowerSet_symm_apply, supIrred_iff_of_finite, OrderIso.supIrredLowerSet_apply, OrderEmbedding.supIrredLowerSet_surjective, supIrred_Iic
|
completelyDistribLattice 📖 | CompOp | 2 mathmath: disjoint_coe, disjoint_prod
|
instBot 📖 | CompOp | 14 mathmath: bot_prod, bot_lt_Iic, Iio_bot, coe_eq_empty, lowerClosure_eq_bot_iff, lowerClosure_empty, Iio_eq_bot, prod_eq_bot, notMem_bot, prod_le_prod_iff, prod_bot, UpperSet.compl_bot, compl_bot, coe_bot
|
instCompleteLinearOrder 📖 | CompOp | — |
instInfSet 📖 | CompOp | 17 mathmath: compl_iInf, compl_iInf₂, Iic_iInf, coe_iicsInfHom, mem_iInf₂_iff, iicsInfHom_apply, coe_sInf, Iic_iInf₂, coe_iInf₂, coe_iInf, Iic_sInf, mem_sInf_iff, compl_sInf, UpperSet.compl_iInf, UpperSet.compl_iInf₂, UpperSet.compl_sInf, mem_iInf_iff
|
instInhabited 📖 | CompOp | — |
instLinearOrder 📖 | CompOp | — |
instMax 📖 | CompOp | 11 mathmath: lowerClosure_union, sup_prod, UpperSet.compl_sup, Iic_sup_erase, coe_sup, lowerClosure_sup_sdiff, erase_sup_Iic, prod_sup, sdiff_sup_lowerClosure, compl_sup, mem_sup_iff
|
instMin 📖 | CompOp | 11 mathmath: inf_prod, mem_inf_iff, lowerClosure_infs, compl_inf, coe_inf, iicInfHom_apply, UpperSet.compl_inf, prod_inf_prod, coe_iicInfHom, prod_inf, Iic_inf
|
instPartialOrder 📖 | CompOp | 39 mathmath: OrderEmbedding.supIrredLowerSet_apply, map_Iio, compl_map, erase_le, coe_subset_coe, upperSetIsoLowerSet_apply, prod_self_lt_prod_self, sdiff_le_left, disjoint_coe, lowerClosure_image, Iio_strictMono, bot_lt_Iic, coe_map, total_le, OrderIso.supIrredLowerSet_symm_apply, upperSetIsoLowerSet_symm_apply, sdiff_lt_left, symm_map, coe_ssubset_coe, Iic_strictMono, disjoint_prod, OrderIso.supIrredLowerSet_apply, Iic_le, OrderEmbedding.supIrredLowerSet_surjective, mem_map, compl_le_compl, erase_lt, lowerClosure_le, prod_self_le_prod_self, prod_le_prod_iff, map_refl, UpperSet.compl_map, OrderEmbedding.birkhoffSet_apply, instIsConcreteLE, map_Iic, gc_lowerClosure_coe, map_map, lowerClosure_mono, UpperSet.compl_le_compl
|
instSetLike 📖 | CompOp | 97 mathmath: mem_compl_iff, coe_eq_univ, mem_iSup_iff, IsOpen.lowerClosure, mem_inf_iff, coe_mk, coe_subset_coe, subset_lowerClosure, disjoint_coe, Topology.IsLowerSet.nhdsKer_eq_lowerClosure, coe_sdiff, IsClosed.lowerClosure_pi, IsClopen.lowerClosure_pi, coe_eq_empty, coe_map, Topology.IsScott.lowerClosure_subset_closure, lowerClosure_interior_subset', sdiff_eq_left, coe_Iio, Topology.IsUpper.isClosed_lowerClosure, OrderIso.supIrredLowerSet_symm_apply, coe_sSup, coe_iSup, sdiff_lt_left, mem_lowerClosure, coe_ssubset_coe, coe_sub, mem_top, coe_sup, mem_iInf₂_iff, coe_top, lowerClosure_eq_Iic_csSup, lowerClosure_interior_subset, coe_sInf, UpperSet.coe_compl, Topology.IsUpperSet.closure_eq_lowerClosure, coe_erase, coe_inf, coe_prod, Iic_le, coe_Iic, coe_iInf₂, coe_iInf, lowerClosure_add, coe_lowerClosure, mem_iSup₂_iff, mem_map, IsAntichain.maximal_mem_lowerClosure_iff_mem, mem_Iio_iff, Matroid.setOf_indep_eq, IsLowerSet.lowerClosure, erase_lt, add_lowerClosure, ordConnected_iff_upperClosure_inter_lowerClosure, upperBounds_lowerClosure, mem_Iic_iff, lowerClosure_le, mem_sInf_iff, ext_iff, BddAbove.lowerClosure, notMem_bot, Set.OrdConnected.upperClosure_inter_lowerClosure, coe_compl, IsUpperSet.disjoint_lowerClosure_left, Set.Finite.lowerClosure, coe_add, coe_div, OrderEmbedding.birkhoffSet_apply, lowerClosure_min, instIsConcreteLE, UpperSet.mem_compl_iff, lowerClosure_mul, coe_iSup₂, Finset.Colex.le_iff_sdiff_subset_lowerClosure, coe_nonempty, mem_mk, HasUpperLowerClosure.isOpen_lowerClosure, mul_lowerClosure, Topology.IsLowerSet.nhdsSet_eq_principal_lowerClosure, UpperSet.coe_sdiff, lower, mem_prod, gc_lowerClosure_coe, lowerClosure, IsUpperSet.disjoint_lowerClosure_right, Order.Ideal.coe_toLowerSet, carrier_eq_coe, lowerClosure_eq, closure_lowerClosure_comm_pi, coe_bot, mem_sSup_iff, coe_mul, UpperSet.coe_erase, mem_iInf_iff, erase_eq, bddAbove_lowerClosure, mem_sup_iff
|
instSupSet 📖 | CompOp | 15 mathmath: iSup_Iic, mem_iSup_iff, UpperSet.compl_sSup, compl_iSup₂, coe_sSup, UpperSet.compl_iSup₂, coe_iSup, UpperSet.compl_iSup, mem_iSup₂_iff, lowerClosure_sUnion, compl_iSup, lowerClosure_iUnion, compl_sSup, coe_iSup₂, mem_sSup_iff
|
instTop 📖 | CompOp | 11 mathmath: coe_eq_univ, lowerClosure_eq_top_iff, Iic_top, lowerClosure_univ, mem_top, coe_top, UpperSet.compl_top, top_prod_top, compl_top, Order.Ideal.top_toLowerSet, lowerClosure_eq_top
|
map 📖 | CompOp | 10 mathmath: map_Iio, compl_map, lowerClosure_image, coe_map, symm_map, mem_map, map_refl, UpperSet.compl_map, map_Iic, map_map
|
| Name | Category | Theorems |
|---|
compl 📖 | CompOp | 17 mathmath: compl_sup, upperSetIsoLowerSet_apply, compl_sSup, compl_iSup₂, compl_compl, coe_compl, compl_iSup, compl_top, LowerSet.compl_compl, compl_map, compl_inf, compl_iInf, compl_bot, mem_compl_iff, compl_iInf₂, compl_sInf, compl_le_compl
|
completeLattice 📖 | CompOp | 6 mathmath: OrderEmbedding.infIrredUpperSet_surjective, OrderIso.infIrredUpperSet_symm_apply, OrderEmbedding.infIrredUpperSet_apply, infIrred_Ici, OrderIso.infIrredUpperSet_apply, infIrred_iff_of_finite
|
completelyDistribLattice 📖 | CompOp | 2 mathmath: codisjoint_coe, codisjoint_prod
|
instBot 📖 | CompOp | 10 mathmath: coe_eq_univ, upperClosure_univ, upperClosure_eq_bot_iff, compl_bot, bot_prod_bot, LowerSet.compl_bot, Ici_bot, coe_bot, mem_bot, upperClosure_eq_bot
|
instCompleteLinearOrder 📖 | CompOp | — |
instInfSet 📖 | CompOp | 15 mathmath: LowerSet.compl_iInf, mem_sInf_iff, LowerSet.compl_iInf₂, coe_iInf₂, mem_iInf_iff, coe_iInf, upperClosure_sUnion, LowerSet.compl_sInf, compl_iInf, coe_sInf, upperClosure_iUnion, compl_iInf₂, compl_sInf, mem_iInf₂_iff, iInf_Ici
|
instInhabited 📖 | CompOp | — |
instLinearOrder 📖 | CompOp | — |
instMax 📖 | CompOp | 11 mathmath: compl_sup, upperClosure_sups, mem_sup_iff, Ici_sup, coe_iciSupHom, sup_prod, iciSupHom_apply, coe_sup, prod_sup_prod, LowerSet.compl_sup, prod_sup
|
instMin 📖 | CompOp | 11 mathmath: Ici_inf_erase, mem_inf_iff, coe_inf, LowerSet.compl_inf, erase_inf_Ici, prod_inf, upperClosure_inf_sdiff, sdiff_inf_upperClosure, compl_inf, inf_prod, upperClosure_union
|
instPartialOrder 📖 | CompOp | 49 mathmath: LowerSet.compl_map, MulArchimedeanClass.subgroup_strictAntiOn, ArchimedeanClass.addSubgroup_antitone, upperClosure_image, upperSetIsoLowerSet_apply, OrderEmbedding.infIrredUpperSet_surjective, Ici_lt_top, mem_map, map_map, coe_ssubset_coe, OrderIso.infIrredUpperSet_symm_apply, MulArchimedeanClass.subsemigroup_strictAnti, codisjoint_coe, prod_le_prod_iff, map_refl, upperSetIsoLowerSet_symm_apply, symm_map, OrderEmbedding.infIrredUpperSet_apply, le_Ici, FiniteArchimedeanClass.subsemigroup_eq_addSubgroup, map_Ici, lt_sdiff_left, LowerSet.compl_le_compl, ArchimedeanClass.subsemigroup_strictAnti, gc_upperClosure_coe, OrderIso.infIrredUpperSet_apply, prod_self_le_prod_self, le_erase, prod_self_lt_prod_self, map_Ioi, FiniteArchimedeanClass.addSubgroup_strictAnti, Ioi_strictMono, le_upperClosure, MulArchimedeanClass.subgroup_antitone, compl_map, ArchimedeanClass.addSubgroup_strictAntiOn, FiniteArchimedeanClass.submodule_strictAnti, coe_map, FiniteMulArchimedeanClass.subsemigroup_eq_subgroup, Ici_le_Ioi, le_sdiff_left, codisjoint_prod, coe_subset_coe, FiniteMulArchimedeanClass.subgroup_strictAnti, lt_erase, total_le, upperClosure_anti, compl_le_compl, Ici_strictMono
|
instSetLike 📖 | CompOp | 101 mathmath: mem_Ioi_iff, coe_Ici, erase_eq, LowerSet.mem_compl_iff, coe_one, ClopenUpperSet.coe_toUpperSet, upperClosure_eq, mem_inf_iff, BddBelow.upperClosure, FiniteArchimedeanClass.mem_addSubgroup_iff, mem_sInf_iff, bddBelow_upperClosure, Topology.IsUpperSet.nhdsKer_eq_upperClosure, sdiff_eq_left, coe_add, IsClosed.upperClosure, carrier_eq_coe, IsUpperSet.upperClosure, LowerSet.coe_sdiff, mem_iSup_iff, IsClopen.upperClosure_pi, mem_map, Topology.IsLowerSet.closure_eq_upperClosure, coe_inf, subset_upperClosure, coe_ssubset_coe, add_upperClosure, ext_iff, coe_eq_empty, upperClosure_interior_subset', OrderIso.infIrredUpperSet_symm_apply, coe_div, MulArchimedeanClass.mem_subgroup_iff, codisjoint_coe, upperClosure_interior_subset, mem_sup_iff, notMem_top, coe_prod, Topology.IsLower.isClosed_upperClosure, mem_Ici_iff, coe_mk, PrimitiveSpectrum.hull_finsetInf, upperClosure_mul, closure_upperClosure_comm_pi, lowerBounds_upperClosure, coe_iInf₂, mem_sSup_iff, coe_eq_univ, coe_compl, le_Ici, upperClosure_min, LowerSet.coe_erase, ArchimedeanClass.mem_addSubgroup_iff, mem_iInf_iff, coe_mul, IsAntichain.minimal_mem_upperClosure_iff_mem, lt_sdiff_left, upperClosure, IsOpen.upperClosure, coe_zero, Topology.IsUpperSet.nhdsSet_eq_principal_upperClosure, PrimitiveSpectrum.preimage_upperClosure_compl_finset, gc_upperClosure_coe, coe_top, coe_iSup, mem_iSup₂_iff, FiniteMulArchimedeanClass.mem_subgroup_iff, ordConnected_iff_upperClosure_inter_lowerClosure, mem_mk, coe_iInf, IsLowerSet.disjoint_upperClosure_left, coe_sub, IsLowerSet.disjoint_upperClosure_right, HasUpperLowerClosure.isOpen_upperClosure, coe_iSup₂, coe_nonempty, mem_prod, coe_upperClosure, coe_sup, upperClosure_add, Set.OrdConnected.upperClosure_inter_lowerClosure, LowerSet.coe_compl, le_upperClosure, upper, coe_map, coe_Ioi, mem_compl_iff, coe_sInf, mul_upperClosure, coe_sSup, coe_sdiff, Set.Finite.upperClosure, coe_subset_coe, IsClosed.upperClosure_pi, lt_erase, mem_iInf₂_iff, coe_bot, coe_erase, mem_bot, mem_upperClosure, upperClosure_eq_Ici_csInf
|
instSupSet 📖 | CompOp | 17 mathmath: mem_iSup_iff, compl_sSup, Ici_iSup, LowerSet.compl_iSup₂, compl_iSup₂, Ici_sSup, mem_sSup_iff, compl_iSup, coe_icisSupHom, icisSupHom_apply, coe_iSup, mem_iSup₂_iff, LowerSet.compl_iSup, coe_iSup₂, LowerSet.compl_sSup, coe_sSup, Ici_iSup₂
|
instTop 📖 | CompOp | 20 mathmath: MulArchimedeanClass.subgroup_strictAntiOn, Ici_lt_top, coe_eq_empty, Ioi_top, prod_le_prod_iff, notMem_top, prod_top, top_prod, Ioi_eq_top, upperClosure_eq_top_iff, compl_top, ArchimedeanClass.addSubgroup_eq_bot, LowerSet.compl_top, upperClosure_empty, coe_top, FiniteMulArchimedeanClass.subgroup_eq_bot, ArchimedeanClass.addSubgroup_strictAntiOn, MulArchimedeanClass.subgroup_eq_bot, FiniteArchimedeanClass.addSubgroup_eq_bot, prod_eq_top
|
map 📖 | CompOp | 10 mathmath: LowerSet.compl_map, upperClosure_image, mem_map, map_map, map_refl, symm_map, map_Ici, map_Ioi, compl_map, coe_map
|