Finset

📁 Source: Mathlib/Order/CompleteLattice/Finset.lean

Statistics

Metric	Count
Definitions	0
Theorems iInf_biUnion, iInf_coe, iInf_finset_image, iInf_insert, iInf_insert_update, iInf_option_toFinset, iInf_singleton, iInf_union, iSup_biUnion, iSup_coe, iSup_finset_image, iSup_insert, iSup_insert_update, iSup_option_toFinset, iSup_singleton, iSup_union, maximal_iff_forall_insert, minimal_iff_forall_diff_singleton, set_biInter_biUnion, set_biInter_coe, set_biInter_finset_image, set_biInter_insert, set_biInter_insert_update, set_biInter_inter, set_biInter_option_toFinset, set_biInter_singleton, set_biUnion_biUnion, set_biUnion_coe, set_biUnion_finset_image, set_biUnion_insert, set_biUnion_insert_update, set_biUnion_option_toFinset, set_biUnion_preimage_singleton, set_biUnion_singleton, set_biUnion_union, subset_set_biUnion_of_mem, iInter_eq_iInter_finset, iInter_eq_iInter_finset', iUnion_eq_iUnion_finset, iUnion_eq_iUnion_finset', iUnion_finset_eq_set, iInf_eq_iInf_finset, iInf_eq_iInf_finset', iSup_eq_iSup_finset, iSup_eq_iSup_finset'	45
Total	45

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf_biUnion 📖	mathematical	—	iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Finset instMembership biUnion	—	iSup_biUnion
iInf_coe 📖	mathematical	—	iInf Set Set.instMembership SetLike.coe Finset instSetLike instMembership	—	—
iInf_finset_image 📖	mathematical	—	iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Finset instMembership image	—	iInf_coe coe_image iInf_image
iInf_insert 📖	mathematical	—	iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Finset instMembership instInsert SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice	—	iSup_insert
iInf_insert_update 📖	mathematical	Finset instMembership	iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf instInsert Function.update SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice	—	iSup_insert_update
iInf_option_toFinset 📖	mathematical	—	iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Finset instMembership Option.toFinset	—	iSup_option_toFinset
iInf_singleton 📖	mathematical	—	iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Finset instMembership instSingleton	—	iInf_congr_Prop iInf_iInf_eq_left
iInf_union 📖	mathematical	—	iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Finset instMembership instUnion SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice	—	iSup_union
iSup_biUnion 📖	mathematical	—	iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Finset instMembership biUnion	—	iSup_congr_Prop iSup_exists iSup_and iSup_comm
iSup_coe 📖	mathematical	—	iSup Set Set.instMembership SetLike.coe Finset instSetLike instMembership	—	—
iSup_finset_image 📖	mathematical	—	iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Finset instMembership image	—	iSup_coe coe_image iSup_image
iSup_insert 📖	mathematical	—	iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Finset instMembership instInsert SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice	—	insert_eq iSup_union iSup_singleton
iSup_insert_update 📖	mathematical	Finset instMembership	iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instInsert Function.update SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice	—	iSup_insert Function.update_self Function.update_of_ne
iSup_option_toFinset 📖	mathematical	—	iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Finset instMembership Option.toFinset	—	iSup_congr_Prop
iSup_singleton 📖	mathematical	—	iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Finset instMembership instSingleton	—	iSup_congr_Prop iSup_iSup_eq_left
iSup_union 📖	mathematical	—	iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Finset instMembership instUnion SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice	—	iSup_congr_Prop iSup_or iSup_sup_eq
maximal_iff_forall_insert 📖	mathematical	—	Maximal Finset Preorder.toLE PartialOrder.toPreorder partialOrder instInsert	—	subset_insert mem_insert_self by_contra insert_subset
minimal_iff_forall_diff_singleton 📖	mathematical	—	Minimal Finset Preorder.toLE PartialOrder.toPreorder partialOrder erase	—	Minimal.prop Minimal.le_of_le erase_subset by_contra subset_erase
set_biInter_biUnion 📖	mathematical	—	Set.iInter Finset instMembership biUnion	—	iInf_biUnion
set_biInter_coe 📖	mathematical	—	Set.iInter Set Set.instMembership SetLike.coe Finset instSetLike instMembership	—	—
set_biInter_finset_image 📖	mathematical	—	Set.iInter Finset instMembership image	—	iInf_finset_image
set_biInter_insert 📖	mathematical	—	Set.iInter Finset instMembership instInsert Set Set.instInter	—	iInf_insert
set_biInter_insert_update 📖	mathematical	Finset instMembership	Set.iInter instInsert Function.update Set Set.instInter	—	iInf_insert_update
set_biInter_inter 📖	mathematical	—	Set.iInter Finset instMembership instUnion Set Set.instInter	—	iInf_union
set_biInter_option_toFinset 📖	mathematical	—	Set.iInter Finset instMembership Option.toFinset	—	iInf_option_toFinset
set_biInter_singleton 📖	mathematical	—	Set.iInter Finset instMembership instSingleton	—	iInf_singleton
set_biUnion_biUnion 📖	mathematical	—	Set.iUnion Finset instMembership biUnion	—	iSup_biUnion
set_biUnion_coe 📖	mathematical	—	Set.iUnion Set Set.instMembership SetLike.coe Finset instSetLike instMembership	—	—
set_biUnion_finset_image 📖	mathematical	—	Set.iUnion Finset instMembership image	—	iSup_finset_image
set_biUnion_insert 📖	mathematical	—	Set.iUnion Finset instMembership instInsert Set Set.instUnion	—	iSup_insert
set_biUnion_insert_update 📖	mathematical	Finset instMembership	Set.iUnion instInsert Function.update Set Set.instUnion	—	iSup_insert_update
set_biUnion_option_toFinset 📖	mathematical	—	Set.iUnion Finset instMembership Option.toFinset	—	iSup_option_toFinset
set_biUnion_preimage_singleton 📖	mathematical	—	Set.iUnion Finset instMembership Set.preimage Set Set.instSingletonSet SetLike.coe instSetLike	—	Set.biUnion_preimage_singleton
set_biUnion_singleton 📖	mathematical	—	Set.iUnion Finset instMembership instSingleton	—	iSup_singleton
set_biUnion_union 📖	mathematical	—	Set.iUnion Finset instMembership instUnion Set Set.instUnion	—	iSup_union
subset_set_biUnion_of_mem 📖	mathematical	Finset instMembership	Set Set.instHasSubset Set.iUnion	—	le_iSup_of_le iSup_congr_Prop iSup_pos

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInter_eq_iInter_finset 📖	mathematical	—	iInter Finset Finset.instMembership	—	iInf_eq_iInf_finset
iInter_eq_iInter_finset' 📖	mathematical	—	iInter Finset Finset.instMembership	—	iInf_eq_iInf_finset'
iUnion_eq_iUnion_finset 📖	mathematical	—	iUnion Finset Finset.instMembership	—	iSup_eq_iSup_finset
iUnion_eq_iUnion_finset' 📖	mathematical	—	iUnion Finset Finset.instMembership	—	iSup_eq_iSup_finset'
iUnion_finset_eq_set 📖	mathematical	—	iUnion Finset Elem image Set instMembership SetLike.coe Finset.instSetLike	—	ext

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf_eq_iInf_finset 📖	mathematical	—	iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Finset Finset.instMembership	—	iSup_eq_iSup_finset
iInf_eq_iInf_finset' 📖	mathematical	—	iInf CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf Finset Finset.instMembership	—	iSup_eq_iSup_finset'
iSup_eq_iSup_finset 📖	mathematical	—	iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Finset Finset.instMembership	—	le_antisymm iSup_le le_iSup_of_le le_rfl le_iSup
iSup_eq_iSup_finset' 📖	mathematical	—	iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Finset Finset.instMembership	—	iSup_eq_iSup_finset Function.Surjective.iSup_comp Equiv.surjective

---

← Back to Index