Density

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

Statistics

Metric	Count
Definitions dens	1
Theorems dens_ne_zero, dens_pos, card_mul_dens, dens_cons, dens_disjUnion, dens_empty, dens_eq_card_div_card, dens_eq_one, dens_eq_zero, dens_filter_add_dens_filter_not_eq_dens, dens_image, dens_inter_add_dens_sdiff, dens_inter_add_dens_union, dens_le_dens, dens_le_dens_sdiff_add_dens, dens_le_one, dens_lt_dens, dens_map_equiv, dens_map_le, dens_mono, dens_mul_card, dens_ne_one, dens_ne_zero, dens_pos, dens_sdiff, dens_sdiff_add_dens, dens_sdiff_add_dens_eq_dens, dens_sdiff_add_dens_inter, dens_sdiff_comm, dens_singleton, dens_strictMono, dens_union_add_dens_inter, dens_union_le, dens_union_of_disjoint, dens_univ, le_dens_sdiff, natCast_card_mul_nnratCast_dens, nnratCast_dens, nnratCast_dens_mul_natCast_card	39
Total	40

Finset

Definitions

Name	Category	Theorems
dens 📖	CompOp	51 math math: dens_union_of_disjoint, dens_cons, dens_sdiff_comm, dens_map_le, addConst_le_inv_dens, dens_inter_add_dens_sdiff, card_mul_dens, dens_map_equiv, dens_sdiff_add_dens_inter, dens_union_add_dens_inter, dens_eq_sum_dens_image, dens_le_one, dens_eq_card_div_card, dens_disjiUnion, dens_strictMono, dens_eq_one, dens_sdiff_add_dens, dens_mul_card, dens_empty, dens_biUnion_le, dens_le_dens_sdiff_add_dens, dens_lt_dens, dens_inv, Fintype.expect_ite_mem, mulConst_le_inv_dens, le_dens_sdiff, dens_neg, dens_image, nnratCast_dens, dens_filter_add_dens_filter_not_eq_dens, dens_mono, dens_inter_add_dens_union, dens_singleton, natCast_card_mul_nnratCast_dens, dens_biUnion, dens_eq_zero, dens_sdiff_add_dens_eq_dens, dens_disjUnion, subConst_le_inv_dens, dens_smul_finset, dens_sdiff, dens_eq_sum_dens_fiberwise, Numbering.dens_prefixed, dens_union_le, Nonempty.dens_pos, nnratCast_dens_mul_natCast_card, dens_le_dens, divConst_le_inv_dens, dens_univ, dens_vadd_finset, dens_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_mul_dens 📖	mathematical	—	NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card dens card	—	isEmpty_or_nonempty Fintype.card_eq_zero Nat.cast_zero Unique.instSubsingleton dens_empty MulZeroClass.mul_zero dens.eq_1 mul_div_cancel₀ NNRat.instCharZero Fintype.card_ne_zero
dens_cons 📖	mathematical	Finset instMembership	dens cons NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card	—	card_cons Nat.cast_add Nat.cast_one add_div one_div
dens_disjUnion 📖	mathematical	Disjoint Finset partialOrder instOrderBot	dens disjUnion NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	card_disjUnion Nat.cast_add add_div
dens_empty 📖	mathematical	—	dens Finset instEmptyCollection NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	Nat.cast_zero zero_div
dens_eq_card_div_card 📖	mathematical	—	dens NNRat NNRat.instDiv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card Fintype.card	—	—
dens_eq_one 📖	mathematical	—	dens NNRat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield univ	—	NNRat.instCharZero
dens_eq_zero 📖	mathematical	—	dens NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Finset instEmptyCollection	—	NNRat.instCharZero eq_empty_of_isEmpty
dens_filter_add_dens_filter_not_eq_dens 📖	mathematical	—	NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield dens filter	—	dens_union_of_disjoint disjoint_filter_filter_not filter_union_filter_not_eq
dens_image 📖	mathematical	Function.Bijective	dens image	—	map_eq_image dens_map_equiv
dens_inter_add_dens_sdiff 📖	mathematical	—	NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield dens Finset instInter instSDiff	—	add_comm dens_sdiff_add_dens_inter
dens_inter_add_dens_union 📖	mathematical	—	NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield dens Finset instInter instUnion	—	add_comm dens_union_add_dens_inter
dens_le_dens 📖	mathematical	Finset instHasSubset	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat dens	—	div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero card_mono Nat.cast_nonneg'
dens_le_dens_sdiff_add_dens 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat dens Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Finset instSDiff	—	dens_le_dens subset_union_left dens_sdiff_add_dens
dens_le_one 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat dens AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	isEmpty_or_nonempty Unique.instSubsingleton dens_empty NNRat.instCanonicallyOrderedAdd dens_univ dens_le_dens subset_univ
dens_lt_dens 📖	mathematical	Finset instHasSSubset	NNRat Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat dens	—	div_lt_div_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat Nat.strictMono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero card_lt_card Nat.cast_zero card_le_univ
dens_map_equiv 📖	mathematical	—	dens map Equiv.toEmbedding	—	card_map Fintype.card_congr
dens_map_le 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat dens map	—	isEmpty_or_nonempty Unique.instSubsingleton dens_empty card_map div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass le_refl Nat.cast_zero NNRat.instCharZero Fintype.card_pos Nat.mono_cast Fintype.card_le_of_injective Function.Embedding.inj'
dens_mono 📖	mathematical	—	Monotone Finset NNRat PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat dens	—	dens_le_dens
dens_mul_card 📖	mathematical	—	NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield dens AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card card	—	mul_comm card_mul_dens
dens_ne_one 📖	—	—	—	—	Iff.not dens_eq_one
dens_ne_zero 📖	mathematical	—	Nonempty	—	Iff.not dens_eq_zero nonempty_iff_ne_empty
dens_pos 📖	mathematical	—	NNRat Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield dens Nonempty	—	pos_iff_ne_zero NNRat.instCanonicallyOrderedAdd dens_ne_zero
dens_sdiff 📖	mathematical	Finset instHasSubset	dens instSDiff NNRat instSubNNRat	—	eq_tsub_of_add_eq NNRat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat dens_sdiff_add_dens_eq_dens
dens_sdiff_add_dens 📖	mathematical	—	NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield dens Finset instSDiff instUnion	—	dens_union_of_disjoint sdiff_disjoint sdiff_union_self_eq_union
dens_sdiff_add_dens_eq_dens 📖	mathematical	Finset instHasSubset	NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield dens instSDiff	—	card_sdiff_add_card_eq_card Nat.cast_add add_div
dens_sdiff_add_dens_inter 📖	mathematical	—	NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield dens Finset instSDiff instInter	—	dens_union_of_disjoint disjoint_sdiff_inter sdiff_union_inter
dens_sdiff_comm 📖	mathematical	card	dens Finset instSDiff	—	add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd dens_sdiff_add_dens union_comm
dens_singleton 📖	mathematical	—	dens Finset instSingleton NNRat NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Fintype.card	—	card_singleton Nat.cast_one one_div
dens_strictMono 📖	mathematical	—	StrictMono Finset NNRat PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat dens	—	dens_lt_dens
dens_union_add_dens_inter 📖	mathematical	—	NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield dens Finset instUnion instInter	—	card_union_add_card_inter
dens_union_le 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat dens Finset instUnion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat zero_le' dens_union_add_dens_inter
dens_union_of_disjoint 📖	mathematical	Disjoint Finset partialOrder instOrderBot	dens instUnion NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	disjUnion_eq_union dens_disjUnion
dens_univ 📖	mathematical	—	dens univ NNRat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	div_self NNRat.instCharZero
le_dens_sdiff 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat instSubNNRat dens Finset instSDiff	—	tsub_le_iff_right NNRat.instOrderedSub dens_le_dens_sdiff_add_dens
natCast_card_mul_nnratCast_dens 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card NNRat.cast DivisionSemiring.toNNRatCast dens card	—	NNRat.cast_natCast card_mul_dens
nnratCast_dens 📖	mathematical	—	NNRat.cast DivisionSemiring.toNNRatCast Semifield.toDivisionSemiring dens DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring card Fintype.card	—	NNRat.cast_div NNRat.cast_natCast
nnratCast_dens_mul_natCast_card 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.cast DivisionSemiring.toNNRatCast dens AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card card	—	NNRat.cast_natCast dens_mul_card

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dens_ne_zero 📖	—	Finset.Nonempty	—	—	Finset.dens_ne_zero
dens_pos 📖	mathematical	Finset.Nonempty	NNRat Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Finset.dens	—	Finset.dens_pos

---

← Back to Index