Mathlib Map

Theorems · Theorem · order theory

Finset.card_Ico_add_right

∀ {M : Type u_1} [inst : AddCancelCommMonoid M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M]
  [inst_3 : LocallyFiniteOrder M] [ExistsAddOfLE M] (a b c : M),
  (Finset.Ico (a + c) (b + c)).card = (Finset.Ico a b).card
Defined in
Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Cited by
1 results in Mathlib
Foundations
Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCancelCommMonoidLinearOrderIsOrderedAddMonoidLocallyFiniteOrderExistsAddOfLE
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

card_Ico_zero_add · cited by 0card_Ico_zero_addLinearOrder · cited by 8572LinearOrderFinset.card · cited by 2327Finset.cardIsOrderedAddMonoid · cited by 1659IsOrderedAddMonoidadd_comm · cited by 1535add_commFinset.map · cited by 747Finset.mapadd_assoc · cited by 746add_assocLocallyFiniteOrder · cited by 658LocallyFiniteOrderFinset.ext · cited by 565Finset.extFinset.Ico · cited by 450Finset.IcoExistsAddOfLE · cited by 330ExistsAddOfLEFinset.card_map · cited by 114Finset.card_mapadd_right_comm · cited by 85add_right_commFinset.mem_Ico · cited by 50Finset.mem_IcoAddCancelCommMonoid · cited by 48AddCancelCommMonoidadd_le_add_iff_right · cited by 47add_le_add_iff_rightFinset.card_Ico_add_rightCITED BYCITES

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.