Arithmetic

📁 Source: Mathlib/Data/Set/Card/Arithmetic.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_disjoint_union_of_even_card, exists_disjoint_union_of_even_card_iff, set_encard_biUnion_le, set_ncard_biUnion_le, encard_biUnion, encard_biUnion_le, ncard_biUnion, ncard_biUnion_le, exists_union_disjoint_cardinal_eq_of_infinite, encard_iUnion_le_of_finite, encard_iUnion_le_of_fintype, encard_iUnion_of_finite, exists_union_disjoint_cardinal_eq_iff, exists_union_disjoint_cardinal_eq_of_even, exists_union_disjoint_ncard_eq_of_even, ncard_iUnion_le_of_finite, ncard_iUnion_le_of_fintype, ncard_iUnion_of_finite, finsum_one	19
Total	19

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_disjoint_union_of_even_card 📖	mathematical	Even card	Finset instUnion Disjoint partialOrder instOrderBot	—	exists_subset_card_eq union_sdiff_self_eq_union card_sdiff_of_subset add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
exists_disjoint_union_of_even_card_iff 📖	mathematical	—	Even card Finset instUnion Disjoint partialOrder instOrderBot	—	exists_disjoint_union_of_even_card card_union_of_disjoint
set_encard_biUnion_le 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Set.encard Set.iUnion Finset instMembership sum LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat	—	apply_union_le_sum IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid Set.encard_empty Set.encard_union_le
set_ncard_biUnion_le 📖	mathematical	—	Set.ncard Set.iUnion Finset instMembership sum Nat.instAddCommMonoid	—	apply_union_le_sum IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Set.ncard_empty Set.ncard_union_le

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
encard_iUnion_le_of_finite 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat encard iUnion finsum LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat	—	iUnion_congr_Prop iUnion_true finsum_congr_Prop finsum_true Finite.encard_biUnion_le finite_univ
encard_iUnion_le_of_fintype 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat encard iUnion Finset.sum LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat Finset.univ	—	iUnion_congr_Prop iUnion_true Finset.set_encard_biUnion_le
encard_iUnion_of_finite 📖	mathematical	Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	encard iUnion finsum ENat LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat	—	finsum_mem_univ Finite.encard_biUnion finite_univ iUnion_congr_Prop iUnion_true
exists_union_disjoint_cardinal_eq_iff 📖	mathematical	—	Even ncard Set instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Elem	—	exists_union_disjoint_cardinal_eq_of_even finite_or_infinite ncard_union_eq finite_union Even.add_self Infinite.ncard
exists_union_disjoint_cardinal_eq_of_even 📖	mathematical	Even ncard	Set instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Elem	—	infinite_or_finite Infinite.exists_union_disjoint_cardinal_eq_of_infinite Finset.exists_disjoint_union_of_even_card ncard_eq_toFinset_card Finite.coe_toFinset Cardinal.mk_fintype Fintype.card_coe
exists_union_disjoint_ncard_eq_of_even 📖	mathematical	Even ncard	Set instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	exists_union_disjoint_cardinal_eq_of_even
ncard_iUnion_le_of_finite 📖	mathematical	—	ncard iUnion finsum Nat.instAddCommMonoid	—	iUnion_congr_Prop iUnion_true finsum_congr_Prop finsum_true Finite.ncard_biUnion_le finite_univ
ncard_iUnion_le_of_fintype 📖	mathematical	—	ncard iUnion Finset.sum Nat.instAddCommMonoid Finset.univ	—	iUnion_congr_Prop iUnion_true Finset.set_ncard_biUnion_le
ncard_iUnion_of_finite 📖	mathematical	Finite Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	ncard iUnion finsum Nat.instAddCommMonoid	—	finsum_mem_univ Finite.ncard_biUnion finite_univ iUnion_congr_Prop iUnion_true

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
encard_biUnion 📖	mathematical	Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.encard Set.iUnion Set.instMembership finsum ENat LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat	—	biUnion cast_ncard_eq ncard_biUnion finsum_mem_congr Nat.cast_finsum_mem Mathlib.Tactic.Push.not_forall_eq Set.insert_diff_self_of_mem finsum_mem_insert Set.notMem_diff_of_mem Set.mem_singleton diff Set.iUnion_congr_Prop Set.insert_diff_singleton Set.iUnion_iUnion_eq_or_left Set.Infinite.encard_eq finsum_congr_Prop top_add
encard_biUnion_le 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Set.encard Set.iUnion Set Set.instMembership finsum LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat	—	Set.iUnion_congr_Prop Finset.set_encard_biUnion_le
ncard_biUnion 📖	mathematical	Set.Finite Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.ncard Set.iUnion Set.instMembership finsum Nat.instAddCommMonoid	—	finsum_one finsum_mem_biUnion finsum_mem_congr
ncard_biUnion_le 📖	mathematical	—	Set.ncard Set.iUnion Set Set.instMembership finsum Nat.instAddCommMonoid	—	Set.iUnion_congr_Prop Finset.set_ncard_biUnion_le

Set.Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_union_disjoint_cardinal_eq_of_infinite 📖	mathematical	Set.Infinite	Set Set.instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.Elem	—	to_subtype Cardinal.eq Cardinal.add_def Cardinal.add_mk_eq_self Set.range_inl_union_range_inr Set.image_univ Subtype.range_coe_subtype Set.disjoint_image_of_injective Subtype.val_injective Disjoint.preimage IsCompl.disjoint Set.isCompl_range_inl_range_inr Cardinal.mk_image_eq Cardinal.mk_preimage_equiv Cardinal.mk_range_inl Cardinal.lift_id Cardinal.mk_range_inr

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finsum_one 📖	mathematical	—	finsum Nat.instAddCommMonoid Set Set.instMembership Set.ncard	—	Set.infinite_or_finite Set.Infinite.ncard finsum_congr_Prop finsum_zero finsum_mem_eq_zero_of_infinite Function.support_const Set.inter_univ finsum_mem_eq_finite_toFinset_sum Finset.sum_const mul_one Set.ncard_eq_toFinset_card

---

← Back to Index