BooleanAlgebra

📁 Source: Mathlib/Data/Finset/BooleanAlgebra.lean

Statistics

Metric	Count
Definitions booleanAlgebra, boundedOrder, decidableCodisjoint, decidableIsCompl	4
Theorems eq_univ, codisjoint_left, codisjoint_right, coe_compl, coe_filter_univ, compl_empty, compl_eq_empty_iff, compl_eq_univ_iff, compl_eq_univ_sdiff, compl_erase, compl_filter, compl_insert, compl_inter, compl_ne_univ_iff_nonempty, compl_singleton, compl_ssubset_compl, compl_subset_compl, compl_union, compl_univ, filter_univ_mem, image_univ_equiv, image_univ_of_surjective, insert_compl_insert, insert_compl_self, insert_inj_on', inter_compl, inter_eq_univ, inter_univ, map_univ_equiv, map_univ_of_surjective, mem_compl, notMem_compl, sdiff_eq_inter_compl, singleton_eq_univ, singleton_ne_univ, ssubset_univ_iff, subset_compl_comm, subset_compl_iff_disjoint_left, subset_compl_iff_disjoint_right, subset_compl_singleton, subtype_eq_univ, subtype_univ, top_eq_univ, union_compl, univ_eq_empty, univ_eq_empty_iff, univ_filter_exists, univ_filter_mem_range, univ_inter, univ_map_equiv_to_embedding, univ_map_subtype, univ_nonempty, univ_nonempty_iff, univ_nontrivial, univ_nontrivial_iff, univ_subset_iff, univ_unique, univ_val_map_subtype_restrict, univ_val_map_subtype_val	59
Total	63

Finset

Definitions

Name	Category	Theorems
booleanAlgebra 📖	CompOp	117 math math: insert_compl_self, compl_ssubset_compl, MeasureTheory.GridLines.T_lmarginal_antitone, SSet.horn₃₁.desc.multicofork_π_two, Ioi_disjUnion_Iio, Equiv.Perm.support_prod_of_pairwise_disjoint, compl_inter, SSet.horn.faceSingletonComplIso_inv_ι_assoc, compl_eq_univ_sdiff, card_compl_add_card, Fin.image_succ_univ, Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub, Set.toFinset_compl, insert_compl_insert, SSet.horn₃₂.desc.multicofork_π_one, sized_compls, union_compl, Matrix.adjp_apply, card_add_card_compl, compl_erase, inclusion_exclusion_card_inf_compl, compl_union, shadow_compls, card_compl, compl_singleton, SimpleGraph.neighborFinset_completeEquipartiteGraph, Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub, SSet.horn₃₁.desc.multicofork_pt, SimpleGraph.neighborFinset_compl, SSet.horn.faceSingletonComplIso_inv_ι, inter_compl, SSet.stdSimplex.range_δ, NumberField.InfinitePlace.card_eq_card_isUnramifiedIn, Fintype.prod_add, subset_compl_singleton, piecewise_compl, inclusion_exclusion_sum_inf_compl, SSet.horn₃₁.desc.multicofork_π_two_assoc, Affine.Simplex.mongePlane_def, SSet.horn₃₁.desc.multicofork_π_zero_assoc, prod_mul_prod_compl, Affine.Simplex.ExcenterExists.excenterWeights_eq_excenterWeights_iff, Fintype.prod_eq_prod_compl_mul, isCoatom_compl_singleton, SSet.stdSimplex.face_obj, exists_sum_eq_one_iff_pairwise_coprime', compl_insert, Fintype.prod_eq_mul_prod_compl, sum_compl_add_sum, preimage_compl, Affine.Simplex.exsphere_compl, compl_filter, SSet.stdSimplex.faceSingletonComplIso_hom_ι, NumberField.InfinitePlace.card_isUnramified_compl, mem_compl, coe_compl, Affine.Simplex.exradius_compl, compl_univ, Equiv.Perm.card_compl_support_modEq, Set.Sized.compls, compl_empty, prod_prod_Ioi_mul_eq_prod_prod_off_diag, SSet.face_le_horn, orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb, Set.powersetCard.coe_compl, AhlswedeZhang.infSum_compls_add_supSum, SSet.horn.faceι_ι, Fin.image_castSucc, SSet.horn_eq_iSup, SimpleGraph.sdiff_compl_neighborFinset_inter_eq, SSet.horn₃₂.desc.multicofork_π_zero_assoc, sum_sum_Ioi_add_eq_sum_sum_off_diag, compl_eq_univ_iff, Fintype.sum_eq_sum_compl_add, SSet.horn.faceι_ι_assoc, mem_inf, Equiv.Perm.support_prod_le, SSet.horn.multicoequalizerDiagram, SSet.horn₃₁.desc.multicofork_π_three_assoc, subset_compl_comm, card_compl_lt_iff_nonempty, SSet.horn₃₁.desc.multicofork_π_zero, SSet.stdSimplex.ofSimplex_yonedaEquiv_δ, SSet.horn₃₂.desc.multicofork_π_three, Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc, upShadow_compls, SSet.boundary_eq_iSup, Set.powersetCard.coe_mulActionHom_compl, isCoatom_iff, SSet.horn₃₂.desc.multicofork_pt, Affine.Simplex.excenterExists_compl, SimpleGraph.compl_neighborFinset_sdiff_inter_eq, Fintype.sum_eq_add_sum_compl, Fin.image_succAbove_univ, prod_compl_mul_prod, subset_compl_iff_disjoint_left, Affine.Simplex.excenterWeightsUnnorm_compl, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, Fintype.not_linearIndependent_iffₒₛ, Affine.Simplex.excenter_compl, sum_add_sum_compl, SSet.horn₃₁.desc.multicofork_π_three, Affine.Simplex.ExcenterExists.excenter_eq_excenter_iff, compl_subset_compl, sdiff_eq_inter_compl, Affine.Simplex.faceOppositeCentroid_eq_affineCombination, Affine.Simplex.excenterWeights_compl, SSet.stdSimplex.face_singleton_compl, compl_eq_empty_iff, subset_compl_iff_disjoint_right, card_truncatedSup_union_add_card_truncatedSup_infs, notMem_compl, insert_inj_on', Set.Finite.toFinset_compl
boundedOrder 📖	CompOp	4 math math: top_eq_univ, codisjoint_left, codisjoint_right, card_truncatedInf_union_add_card_truncatedInf_sups
decidableCodisjoint 📖	CompOp	—
decidableIsCompl 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codisjoint_left 📖	mathematical	—	Codisjoint Finset partialOrder BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder boundedOrder instMembership	—	—
codisjoint_right 📖	mathematical	—	Codisjoint Finset partialOrder BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder boundedOrder instMembership	—	codisjoint_comm codisjoint_left
coe_compl 📖	mathematical	—	SetLike.coe Finset instSetLike Compl.compl BooleanAlgebra.toCompl booleanAlgebra Set Set.instCompl	—	Set.ext mem_compl
coe_filter_univ 📖	mathematical	—	SetLike.coe Finset instSetLike filter univ setOf	—	coe_filter
compl_empty 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra instEmptyCollection univ	—	compl_bot
compl_eq_empty_iff 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra instEmptyCollection univ	—	compl_eq_bot
compl_eq_univ_iff 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra univ instEmptyCollection	—	compl_eq_top
compl_eq_univ_sdiff 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra instSDiff univ	—	—
compl_erase 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra erase instInsert	—	ext
compl_filter 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra filter univ	—	ext
compl_insert 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra instInsert erase	—	ext
compl_inter 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra instInter instUnion	—	compl_inf
compl_ne_univ_iff_nonempty 📖	mathematical	—	Nonempty	—	—
compl_singleton 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra instSingleton erase univ	—	compl_eq_univ_sdiff sdiff_singleton_eq_erase
compl_ssubset_compl 📖	mathematical	—	Finset instHasSSubset Compl.compl BooleanAlgebra.toCompl booleanAlgebra	—	compl_lt_compl_iff_lt
compl_subset_compl 📖	mathematical	—	Finset instHasSubset Compl.compl BooleanAlgebra.toCompl booleanAlgebra	—	compl_le_compl_iff_le
compl_union 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra instUnion instInter	—	compl_sup
compl_univ 📖	mathematical	—	Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra univ instEmptyCollection	—	compl_top
filter_univ_mem 📖	mathematical	—	filter Finset instMembership decidableMem univ	—	filter_mem_eq_inter univ_inter
image_univ_equiv 📖	mathematical	—	image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike univ	—	image_univ_of_surjective Equiv.surjective
image_univ_of_surjective 📖	mathematical	—	image univ	—	eq_univ_of_forall Function.Surjective.forall mem_image_of_mem mem_univ
insert_compl_insert 📖	mathematical	Finset instMembership	instInsert Compl.compl BooleanAlgebra.toCompl booleanAlgebra	—	compl_insert insert_erase mem_compl
insert_compl_self 📖	mathematical	—	Finset instInsert Compl.compl BooleanAlgebra.toCompl booleanAlgebra instSingleton univ	—	compl_erase erase_singleton compl_empty
insert_inj_on' 📖	mathematical	—	Set.InjOn Finset instInsert SetLike.coe instSetLike Compl.compl BooleanAlgebra.toCompl booleanAlgebra	—	coe_compl insert_inj_on
inter_compl 📖	mathematical	—	Finset instInter Compl.compl BooleanAlgebra.toCompl booleanAlgebra instEmptyCollection	—	inf_compl_eq_bot
inter_eq_univ 📖	mathematical	—	Finset instInter univ	—	inf_eq_top_iff
inter_univ 📖	mathematical	—	Finset instInter univ	—	inter_comm univ_inter
map_univ_equiv 📖	mathematical	—	map Equiv.toEmbedding univ	—	map_univ_of_surjective Equiv.surjective
map_univ_of_surjective 📖	mathematical	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	map univ	—	eq_univ_of_forall Function.Surjective.forall mem_map_of_mem mem_univ
mem_compl 📖	mathematical	—	Finset instMembership Compl.compl BooleanAlgebra.toCompl booleanAlgebra	—	—
notMem_compl 📖	mathematical	—	Finset instMembership Compl.compl BooleanAlgebra.toCompl booleanAlgebra	—	mem_compl
sdiff_eq_inter_compl 📖	mathematical	—	Finset instSDiff instInter Compl.compl BooleanAlgebra.toCompl booleanAlgebra	—	sdiff_eq
singleton_eq_univ 📖	mathematical	—	Finset instSingleton univ	—	ext
singleton_ne_univ 📖	—	—	—	—	SetLike.coe_ne_coe coe_singleton coe_univ
ssubset_univ_iff 📖	mathematical	—	Finset instHasSSubset univ	—	lt_top_iff_ne_top
subset_compl_comm 📖	mathematical	—	Finset instHasSubset Compl.compl BooleanAlgebra.toCompl booleanAlgebra	—	le_compl_iff_le_compl
subset_compl_iff_disjoint_left 📖	mathematical	—	Finset instHasSubset Compl.compl BooleanAlgebra.toCompl booleanAlgebra Disjoint partialOrder instOrderBot	—	le_compl_iff_disjoint_left
subset_compl_iff_disjoint_right 📖	mathematical	—	Finset instHasSubset Compl.compl BooleanAlgebra.toCompl booleanAlgebra Disjoint partialOrder instOrderBot	—	le_compl_iff_disjoint_right
subset_compl_singleton 📖	mathematical	—	Finset instHasSubset Compl.compl BooleanAlgebra.toCompl booleanAlgebra instSingleton instMembership	—	subset_compl_comm singleton_subset_iff mem_compl
subtype_eq_univ 📖	mathematical	—	subtype univ Finset instMembership	—	—
subtype_univ 📖	mathematical	—	subtype univ	—	—
top_eq_univ 📖	mathematical	—	Top.top Finset OrderTop.toTop Preorder.toLE PartialOrder.toPreorder partialOrder BoundedOrder.toOrderTop boundedOrder univ	—	—
union_compl 📖	mathematical	—	Finset instUnion Compl.compl BooleanAlgebra.toCompl booleanAlgebra univ	—	sup_compl_eq_top
univ_eq_empty 📖	mathematical	—	univ Finset instEmptyCollection	—	univ_eq_empty_iff
univ_eq_empty_iff 📖	mathematical	—	univ Finset instEmptyCollection IsEmpty	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ univ_nonempty_iff
univ_filter_exists 📖	mathematical	—	filter univ image	—	ext
univ_filter_mem_range 📖	mathematical	—	filter Set Set.instMembership Set.range univ image	—	—
univ_inter 📖	mathematical	—	Finset instInter univ	—	ext
univ_map_equiv_to_embedding 📖	mathematical	—	map Equiv.toEmbedding univ	—	eq_univ_iff_forall mem_map mem_univ Equiv.apply_symm_apply
univ_map_subtype 📖	mathematical	—	map Function.Embedding.subtype univ filter	—	subtype_map subtype_univ
univ_nonempty 📖	mathematical	—	Nonempty univ	—	univ_nonempty_iff
univ_nonempty_iff 📖	mathematical	—	Nonempty univ	—	coe_nonempty coe_univ Set.nonempty_iff_univ_nonempty
univ_nontrivial 📖	mathematical	—	Nontrivial univ	—	univ_nontrivial_iff
univ_nontrivial_iff 📖	mathematical	—	Nontrivial univ Nontrivial	—	Nontrivial.eq_1 coe_univ Set.nontrivial_univ_iff
univ_subset_iff 📖	mathematical	—	Finset instHasSubset univ	—	top_le_iff
univ_unique 📖	mathematical	—	univ Finset instSingleton Unique.instInhabited	—	ext mem_univ mem_singleton Unique.instSubsingleton
univ_val_map_subtype_restrict 📖	mathematical	—	Multiset.map Subtype.restrict val univ filter	—	univ_val_map_subtype_val Multiset.map_map Subtype.restrict_def
univ_val_map_subtype_val 📖	mathematical	—	Multiset.map val univ filter	—	map_val univ_map_subtype

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_univ 📖	mathematical	Finset.Nonempty	Finset.univ	—	Finset.eq_univ_of_forall

---

← Back to Index