mathlib documentation

data.fintype.powerset

fintype instance for set α, when α is a fintype #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
def finset.fintype {α : Type u_1} [fintype α] :
Equations
@[simp]
theorem fintype.card_finset {α : Type u_1} [fintype α] :
@[simp]
theorem finset.powerset_eq_univ {α : Type u_1} [fintype α] {s : finset α} :
@[simp]
@[simp]
theorem fintype.card_finset_len {α : Type u_1} [fintype α] (k : ) :
@[protected, instance]
def set.fintype {α : Type u_1} [fintype α] :
Equations
@[protected, instance]
def set.finite' {α : Type u_1} [finite α] :
finite (set α)
@[simp]
theorem fintype.card_set {α : Type u_1} [fintype α] :