NAry

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

Statistics

Metric	Count
Definitions image₂	1
Theorems image₂, of_image₂_left, of_image₂_right, biUnion_image_left, biUnion_image_right, card_dvd_card_image₂_left, card_dvd_card_image₂_right, card_image₂, card_image₂_iff, card_image₂_le, card_image₂_singleton_left, card_image₂_singleton_right, card_le_card_image₂_left, card_le_card_image₂_right, coe_image₂, exists_mem_image₂, forall_mem_image₂, image_image₂, image_image₂_antidistrib, image_image₂_antidistrib_left, image_image₂_antidistrib_right, image_image₂_distrib, image_image₂_distrib_left, image_image₂_distrib_right, image_image₂_right_anticomm, image_image₂_right_comm, image_subset_image₂_left, image_subset_image₂_right, image_uncurry_product, image₂_assoc, image₂_comm, image₂_congr, image₂_congr', image₂_curry, image₂_distrib_subset_left, image₂_distrib_subset_right, image₂_empty_left, image₂_empty_right, image₂_eq_empty_iff, image₂_image_left, image₂_image_left_anticomm, image₂_image_left_comm, image₂_image_right, image₂_image₂_image₂_comm, image₂_insert_left, image₂_insert_right, image₂_inter_left, image₂_inter_right, image₂_inter_singleton, image₂_inter_subset_left, image₂_inter_subset_right, image₂_inter_union_subset, image₂_inter_union_subset_union, image₂_left, image₂_left_comm, image₂_left_identity, image₂_mk_eq_product, image₂_nonempty_iff, image₂_right, image₂_right_comm, image₂_right_identity, image₂_singleton, image₂_singleton_inter, image₂_singleton_left, image₂_singleton_left', image₂_singleton_right, image₂_subset, image₂_subset_iff, image₂_subset_iff_left, image₂_subset_iff_right, image₂_subset_left, image₂_subset_right, image₂_swap, image₂_union_inter_subset, image₂_union_inter_subset_union, image₂_union_left, image₂_union_right, inf'_image₂_left, inf'_image₂_right, inf_image₂_left, inf_image₂_right, le_inf'_image₂, le_inf_image₂, mem_image₂, mem_image₂_iff, mem_image₂_of_mem, subset_set_image₂, sup'_image₂_le, sup'_image₂_left, sup'_image₂_right, sup_image₂_le, sup_image₂_left, sup_image₂_right, piFinset_image₂, toFinset_image2, toFinset_image2	96
Total	97

Finset

Definitions

Name	Category	Theorems
image₂ 📖	CompOp	90 math math: image_image₂, image₂_inter_singleton, image₂_curry, image_uncurry_product, biUnion_image_left, image₂_inter_right, card_image₂, image_image₂_antidistrib_right, image₂_left_identity, image₂_eq_empty_iff, image₂_subset_iff_right, image₂_congr, card_image₂_singleton_left, card_image₂_le, image_vsub_product, le_inf_image₂, image₂_insert_left, image₂_subset_iff, image₂_empty_right, image₂_def, image₂_inter_union_subset, image₂_image_left, Set.toFinset_image2, image_image₂_distrib_right, exists_mem_image₂, card_image₂_singleton_right, card_dvd_card_image₂_left, image₂_swap, mem_image₂, inf_image₂_left, mem_image₂_of_mem, image₂_union_inter_subset_union, image₂_comm, image₂_empty_left, image₂_subset_right, image₂_inter_union_subset_union, image₂_distrib_subset_right, image₂_union_left, image₂_inter_subset_right, image_subset_image₂_left, Nonempty.image₂, image₂_image_left_anticomm, image₂_distrib_subset_left, Fintype.piFinset_image₂, image_image₂_antidistrib, image₂_singleton_left, image₂_left_comm, image₂_inter_subset_left, image₂_union_inter_subset, card_dvd_card_image₂_right, image₂_image₂_image₂_comm, biUnion_image_right, image₂_subset_iff_left, image₂_image_left_comm, image₂_inter_left, image₂_right_comm, subset_set_image₂, image₂_left, card_le_card_image₂_right, image₂_singleton_left', image₂_singleton_right, image₂_subset, image_subset_image₂_right, card_image₂_iff, image₂_mk_eq_product, image₂_subset_left, inf_image₂_right, mem_image₂_iff, image₂_insert_right, card_le_card_image₂_left, image₂_assoc, image₂_congr', image₂_right, sup_image₂_le, image₂_nonempty_iff, image₂_union_right, image_image₂_right_comm, sup_image₂_right, image₂_right_identity, Set.Finite.toFinset_image2, coe_image₂, image_image₂_right_anticomm, image_image₂_distrib_left, image₂_singleton_inter, image_image₂_antidistrib_left, image_image₂_distrib, image₂_singleton, vsub_def, image₂_image_right, sup_image₂_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion_image_left 📖	mathematical	—	biUnion image image₂	—	coe_injective coe_biUnion Set.iUnion_congr_Prop coe_image coe_image₂ Set.iUnion_image_left
biUnion_image_right 📖	mathematical	—	biUnion image image₂	—	coe_injective coe_biUnion Set.iUnion_congr_Prop coe_image coe_image₂ Set.iUnion_image_right
card_dvd_card_image₂_left 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot Set.image image SetLike.coe instSetLike	card image₂	—	image₂_swap card_dvd_card_image₂_right
card_dvd_card_image₂_right 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot Set.image image SetLike.coe instSetLike	card image₂	—	induction image₂_empty_left image₂_insert_left card_union_of_disjoint Eq.dvd card_image_of_injective mem_insert_self forall_of_forall_insert Set.PairwiseDisjoint.subset Set.image_mono coe_subset subset_insert union_eq_right Eq.trans_subset Set.Pairwise.eq Set.mem_image_of_mem mem_insert_of_mem image_subset_image₂_right
card_image₂ 📖	mathematical	Function.Injective2	card image₂	—	card_image_of_injective Function.Injective2.uncurry card_product
card_image₂_iff 📖	mathematical	—	card image₂ Set.InjOn SProd.sprod Set Set.instSProd SetLike.coe Finset instSetLike	—	card_product coe_product card_image_iff
card_image₂_le 📖	mathematical	—	card image₂	—	LE.le.trans_eq card_image_le card_product
card_image₂_singleton_left 📖	mathematical	—	card image₂ Finset instSingleton	—	image₂_singleton_left card_image_of_injective
card_image₂_singleton_right 📖	mathematical	—	card image₂ Finset instSingleton	—	image₂_singleton_right card_image_of_injective
card_le_card_image₂_left 📖	mathematical	Finset instMembership	card image₂	—	card_le_card_of_injOn mem_image₂_of_mem Function.Injective.injOn
card_le_card_image₂_right 📖	mathematical	Finset instMembership	card image₂	—	card_le_card_of_injOn mem_image₂_of_mem Function.Injective.injOn
coe_image₂ 📖	mathematical	—	SetLike.coe Finset instSetLike image₂ Set.image2	—	Set.ext mem_image₂
exists_mem_image₂ 📖	mathematical	—	Finset instMembership image₂	—	coe_image₂
forall_mem_image₂ 📖	—	—	—	—	coe_image₂
image_image₂ 📖	mathematical	—	image image₂	—	coe_injective coe_image coe_image₂ Set.image_image2
image_image₂_antidistrib 📖	mathematical	—	image image₂	—	image₂_swap image_image₂_distrib
image_image₂_antidistrib_left 📖	mathematical	—	image image₂	—	coe_injective coe_image coe_image₂ Set.image_image2_antidistrib_left
image_image₂_antidistrib_right 📖	mathematical	—	image image₂	—	coe_injective coe_image coe_image₂ Set.image_image2_antidistrib_right
image_image₂_distrib 📖	mathematical	—	image image₂	—	coe_injective coe_image coe_image₂ Set.image_image2_distrib
image_image₂_distrib_left 📖	mathematical	—	image image₂	—	coe_injective coe_image coe_image₂ Set.image_image2_distrib_left
image_image₂_distrib_right 📖	mathematical	—	image image₂	—	coe_injective coe_image coe_image₂ Set.image_image2_distrib_right
image_image₂_right_anticomm 📖	mathematical	—	image₂ image	—	image_image₂_antidistrib_right
image_image₂_right_comm 📖	mathematical	—	image₂ image	—	image_image₂_distrib_right
image_subset_image₂_left 📖	mathematical	Finset instMembership	instHasSubset image image₂	—	image_subset_iff mem_image₂_of_mem
image_subset_image₂_right 📖	mathematical	Finset instMembership	instHasSubset image image₂	—	image_subset_iff mem_image₂_of_mem
image_uncurry_product 📖	mathematical	—	image SProd.sprod Finset instSProd image₂	—	—
image₂_assoc 📖	mathematical	—	image₂	—	coe_injective coe_image₂ Set.image2_assoc
image₂_comm 📖	mathematical	—	image₂	—	image₂_swap
image₂_congr 📖	mathematical	—	image₂	—	coe_injective coe_image₂ Set.image2_congr
image₂_congr' 📖	mathematical	—	image₂	—	image₂_congr
image₂_curry 📖	mathematical	—	image₂ image SProd.sprod Finset instSProd	—	—
image₂_distrib_subset_left 📖	mathematical	—	Finset instHasSubset image₂	—	coe_subset coe_image₂ Set.image2_distrib_subset_left
image₂_distrib_subset_right 📖	mathematical	—	Finset instHasSubset image₂	—	coe_subset coe_image₂ Set.image2_distrib_subset_right
image₂_empty_left 📖	mathematical	—	image₂ Finset instEmptyCollection	—	coe_injective coe_image₂ coe_empty Set.image2_empty_left
image₂_empty_right 📖	mathematical	—	image₂ Finset instEmptyCollection	—	coe_injective coe_image₂ coe_empty Set.image2_empty_right
image₂_eq_empty_iff 📖	mathematical	—	image₂ Finset instEmptyCollection	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ image₂_nonempty_iff
image₂_image_left 📖	mathematical	—	image₂ image	—	coe_injective coe_image₂ coe_image Set.image2_image_left
image₂_image_left_anticomm 📖	mathematical	—	image₂ image	—	image_image₂_antidistrib_left
image₂_image_left_comm 📖	mathematical	—	image₂ image	—	image_image₂_distrib_left
image₂_image_right 📖	mathematical	—	image₂ image	—	coe_injective coe_image₂ coe_image Set.image2_image_right
image₂_image₂_image₂_comm 📖	mathematical	—	image₂	—	coe_injective coe_image₂ Set.image2_image2_image2_comm
image₂_insert_left 📖	mathematical	—	image₂ Finset instInsert instUnion image	—	coe_injective coe_image₂ coe_insert coe_union coe_image Set.image2_insert_left
image₂_insert_right 📖	mathematical	—	image₂ Finset instInsert instUnion image	—	coe_injective coe_image₂ coe_insert coe_union coe_image Set.image2_insert_right
image₂_inter_left 📖	mathematical	Function.Injective2	image₂ Finset instInter	—	coe_injective coe_image₂ coe_inter Set.image2_inter_left
image₂_inter_right 📖	mathematical	Function.Injective2	image₂ Finset instInter	—	coe_injective coe_image₂ coe_inter Set.image2_inter_right
image₂_inter_singleton 📖	mathematical	—	image₂ Finset instInter instSingleton	—	image₂_singleton_right image_inter
image₂_inter_subset_left 📖	mathematical	—	Finset instHasSubset image₂ instInter	—	coe_subset coe_image₂ coe_inter Set.image2_inter_subset_left
image₂_inter_subset_right 📖	mathematical	—	Finset instHasSubset image₂ instInter	—	coe_subset coe_image₂ coe_inter Set.image2_inter_subset_right
image₂_inter_union_subset 📖	mathematical	—	Finset instHasSubset image₂ instInter instUnion	—	coe_subset coe_image₂ coe_inter coe_union Set.image2_inter_union_subset
image₂_inter_union_subset_union 📖	mathematical	—	Finset instHasSubset image₂ instInter instUnion	—	coe_subset coe_image₂ coe_inter coe_union Set.image2_inter_union_subset_union
image₂_left 📖	mathematical	Nonempty	image₂	—	coe_injective coe_image₂ Set.image2_left
image₂_left_comm 📖	mathematical	—	image₂	—	coe_injective coe_image₂ Set.image2_left_comm
image₂_left_identity 📖	mathematical	—	image₂ Finset instSingleton	—	coe_injective coe_image₂ coe_singleton Set.image2_left_identity
image₂_mk_eq_product 📖	mathematical	—	image₂ SProd.sprod Finset instSProd	—	ext
image₂_nonempty_iff 📖	mathematical	—	Nonempty image₂	—	coe_nonempty coe_image₂ Set.image2_nonempty_iff
image₂_right 📖	mathematical	Nonempty	image₂	—	coe_injective coe_image₂ Set.image2_right
image₂_right_comm 📖	mathematical	—	image₂	—	coe_injective coe_image₂ Set.image2_right_comm
image₂_right_identity 📖	mathematical	—	image₂ Finset instSingleton	—	image₂_singleton_right image_id'
image₂_singleton 📖	mathematical	—	image₂ Finset instSingleton	—	image₂_singleton_right image_singleton
image₂_singleton_inter 📖	mathematical	—	image₂ Finset instSingleton instInter	—	image₂_singleton_left image_inter
image₂_singleton_left 📖	mathematical	—	image₂ Finset instSingleton image	—	ext
image₂_singleton_left' 📖	mathematical	—	image₂ Finset instSingleton image	—	image₂_singleton_left
image₂_singleton_right 📖	mathematical	—	image₂ Finset instSingleton image	—	ext
image₂_subset 📖	mathematical	Finset instHasSubset	image₂	—	coe_subset coe_image₂ Set.image2_subset
image₂_subset_iff 📖	mathematical	—	Finset instHasSubset image₂ instMembership	—	forall_mem_image₂
image₂_subset_iff_left 📖	mathematical	—	Finset instHasSubset image₂ image	—	—
image₂_subset_iff_right 📖	mathematical	—	Finset instHasSubset image₂ image	—	forall₂_swap
image₂_subset_left 📖	mathematical	Finset instHasSubset	image₂	—	image₂_subset Subset.rfl
image₂_subset_right 📖	mathematical	Finset instHasSubset	image₂	—	image₂_subset Subset.rfl
image₂_swap 📖	mathematical	—	image₂	—	coe_injective coe_image₂ Set.image2_swap
image₂_union_inter_subset 📖	mathematical	—	Finset instHasSubset image₂ instUnion instInter	—	coe_subset coe_image₂ coe_union coe_inter Set.image2_union_inter_subset
image₂_union_inter_subset_union 📖	mathematical	—	Finset instHasSubset image₂ instUnion instInter	—	coe_subset coe_image₂ coe_union coe_inter Set.image2_union_inter_subset_union
image₂_union_left 📖	mathematical	—	image₂ Finset instUnion	—	coe_injective coe_image₂ coe_union Set.image2_union_left
image₂_union_right 📖	mathematical	—	image₂ Finset instUnion	—	coe_injective coe_image₂ coe_union Set.image2_union_right
inf'_image₂_left 📖	mathematical	Nonempty image₂	inf' Nonempty.of_image₂_left Nonempty.of_image₂_right	—	sup'_image₂_left
inf'_image₂_right 📖	mathematical	Nonempty image₂	inf' Nonempty.of_image₂_right Nonempty.of_image₂_left	—	sup'_image₂_right
inf_image₂_left 📖	mathematical	—	inf image₂	—	sup_image₂_left
inf_image₂_right 📖	mathematical	—	inf image₂	—	sup_image₂_right
le_inf'_image₂ 📖	mathematical	Nonempty image₂	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder inf'	—	le_inf'_iff forall_mem_image₂
le_inf_image₂ 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder inf image₂	—	sup_image₂_le
mem_image₂ 📖	mathematical	—	Finset instMembership image₂	—	—
mem_image₂_iff 📖	mathematical	Function.Injective2	Finset instMembership image₂	—	mem_coe coe_image₂ Set.mem_image2_iff
mem_image₂_of_mem 📖	mathematical	Finset instMembership	image₂	—	mem_image₂
subset_set_image₂ 📖	mathematical	Set Set.instHasSubset SetLike.coe Finset instSetLike Set.image2	instHasSubset image₂	—	subset_set_image_iff Set.image_prod coe_image image₂_image_right image₂_image_left mem_image₂_of_mem
sup'_image₂_le 📖	mathematical	Nonempty image₂	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder sup'	—	sup'_le_iff forall_mem_image₂
sup'_image₂_left 📖	mathematical	Nonempty image₂	sup' Nonempty.of_image₂_left Nonempty.of_image₂_right	—	Nonempty.of_image₂_left Nonempty.of_image₂_right Nonempty.fst Nonempty.of_image Nonempty.snd sup'_image sup'_product_left
sup'_image₂_right 📖	mathematical	Nonempty image₂	sup' Nonempty.of_image₂_right Nonempty.of_image₂_left	—	Nonempty.of_image₂_right Nonempty.of_image₂_left Nonempty.snd Nonempty.of_image Nonempty.fst sup'_image sup'_product_right
sup_image₂_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder sup image₂	—	sup_le_iff forall_mem_image₂
sup_image₂_left 📖	mathematical	—	sup image₂	—	sup_image sup_product_left
sup_image₂_right 📖	mathematical	—	sup image₂	—	sup_image sup_product_right

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image₂ 📖	mathematical	Finset.Nonempty	Finset.image₂	—	Finset.image₂_nonempty_iff
of_image₂_left 📖	—	Finset.Nonempty Finset.image₂	—	—	Finset.image₂_nonempty_iff
of_image₂_right 📖	—	Finset.Nonempty Finset.image₂	—	—	Finset.image₂_nonempty_iff

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piFinset_image₂ 📖	mathematical	—	piFinset Finset.image₂ decidablePiFintype	—	Finset.ext

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFinset_image2 📖	mathematical	—	toFinset image2 Finset.image₂	—	Finset.coe_injective coe_toFinset Finset.coe_image₂

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFinset_image2 📖	mathematical	—	toFinset Set.image2 Finset.image₂	—	Finset.coe_injective coe_toFinset Finset.coe_image₂

---

← Back to Index