Theorems · Theorem · combinatorics
Fintype.card_subtype_lt
∀ {α : Type u_1} [inst : Fintype α] {p : α → Prop} [inst_1 : Fintype { a // p a }] {x : α},
¬p x → Fintype.card { x // p x } < Fintype.card α- Defined in
- Mathlib.Data.Fintype.Card
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Fintypestatement and proof · cited by 7,736
- Fintype.cardstatement · cited by 1,386
- Subtype.coe_injectiveproof · cited by 205
- Subtype.range_coe_subtypeproof · cited by 170
- Fintype.card_lt_of_injective_of_notMemproof · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquivproof · cited by 1
- Finite.card_subtype_ltproof · cited by 0