Fin-indexed tuples of finsets #
@[deprecated Fin.mem_piFinset_iff_zero_tail]
theorem
Fin.mem_piFinset_succ
{n : ℕ}
{α : Fin (n + 1) → Type u_1}
{f : (i : Fin (n + 1)) → α i}
{s : (i : Fin (n + 1)) → Finset (α i)}
:
f ∈ Fintype.piFinset s ↔ f 0 ∈ s 0 ∧ Fin.tail f ∈ Fintype.piFinset (Fin.tail s)
Alias of Fin.mem_piFinset_iff_zero_tail
.
theorem
Fin.cons_mem_piFinset_cons
{n : ℕ}
{α : Fin (n + 1) → Type u_1}
{x_zero : α 0}
{x_tail : (i : Fin n) → α i.succ}
{s_zero : Finset (α 0)}
{s_tail : (i : Fin n) → Finset (α i.succ)}
:
Fin.cons x_zero x_tail ∈ Fintype.piFinset (Fin.cons s_zero s_tail) ↔ x_zero ∈ s_zero ∧ x_tail ∈ Fintype.piFinset s_tail
theorem
Fin.snoc_mem_piFinset_snoc
{n : ℕ}
{α : Fin (n + 1) → Type u_1}
{x_last : α (Fin.last n)}
{x_init : (i : Fin n) → α i.castSucc}
{s_last : Finset (α (Fin.last n))}
{s_init : (i : Fin n) → Finset (α i.castSucc)}
:
Fin.snoc x_init x_last ∈ Fintype.piFinset (Fin.snoc s_init s_last) ↔ x_last ∈ s_last ∧ x_init ∈ Fintype.piFinset s_init
theorem
Fin.insertNth_mem_piFinset_insertNth
{n : ℕ}
{α : Fin (n + 1) → Type u_1}
{p : Fin (n + 1)}
{x_pivot : α p}
{x_remove : (i : Fin n) → α (p.succAbove i)}
{s_pivot : Finset (α p)}
{s_remove : (i : Fin n) → Finset (α (p.succAbove i))}
:
p.insertNth x_pivot x_remove ∈ Fintype.piFinset (p.insertNth s_pivot s_remove) ↔ x_pivot ∈ s_pivot ∧ x_remove ∈ Fintype.piFinset s_remove
theorem
Finset.map_consEquiv_filter_piFinset
{n : ℕ}
{α : Fin (n + 1) → Type u_1}
(S : (i : Fin (n + 1)) → Finset (α i))
(P : ((i : Fin n) → α i.succ) → Prop)
[DecidablePred P]
:
Finset.map (Fin.consEquiv α).symm.toEmbedding
(Finset.filter (fun (r : (i : Fin (n + 1)) → α i) => P (Fin.tail r)) (Fintype.piFinset S)) = S 0 ×ˢ Finset.filter P (Fintype.piFinset fun (x : Fin n) => S x.succ)
theorem
Finset.map_snocEquiv_filter_piFinset
{n : ℕ}
{α : Fin (n + 1) → Type u_1}
(S : (i : Fin (n + 1)) → Finset (α i))
(P : ((i : Fin n) → α i.castSucc) → Prop)
[DecidablePred P]
:
Finset.map (Fin.snocEquiv α).symm.toEmbedding
(Finset.filter (fun (r : (i : Fin (n + 1)) → α i) => P (Fin.init r)) (Fintype.piFinset S)) = S (Fin.last n) ×ˢ Finset.filter P (Fintype.piFinset (Fin.init S))
theorem
Finset.map_insertNthEquiv_filter_piFinset
{n : ℕ}
{α : Fin (n + 1) → Type u_1}
{p : Fin (n + 1)}
(S : (i : Fin (n + 1)) → Finset (α i))
(P : ((i : Fin n) → α (p.succAbove i)) → Prop)
[DecidablePred P]
:
Finset.map (Fin.insertNthEquiv α p).symm.toEmbedding
(Finset.filter (fun (r : (i : Fin (n + 1)) → α i) => P (p.removeNth r)) (Fintype.piFinset S)) = S p ×ˢ Finset.filter P (Fintype.piFinset (p.removeNth S))
theorem
Finset.card_consEquiv_filter_piFinset
{n : ℕ}
{α : Fin (n + 1) → Type u_1}
(S : (i : Fin (n + 1)) → Finset (α i))
(P : ((i : Fin n) → α i.succ) → Prop)
[DecidablePred P]
:
(Finset.filter (fun (r : (i : Fin (n + 1)) → α i) => P (Fin.tail r)) (Fintype.piFinset S)).card = (S 0).card * (Finset.filter P (Fintype.piFinset fun (x : Fin n) => S x.succ)).card
theorem
Finset.card_snocEquiv_filter_piFinset
{n : ℕ}
{α : Fin (n + 1) → Type u_1}
(S : (i : Fin (n + 1)) → Finset (α i))
(P : ((i : Fin n) → α i.castSucc) → Prop)
[DecidablePred P]
:
(Finset.filter (fun (r : (i : Fin (n + 1)) → α i) => P (Fin.init r)) (Fintype.piFinset S)).card = (S (Fin.last n)).card * (Finset.filter P (Fintype.piFinset (Fin.init S))).card
theorem
Finset.card_insertNthEquiv_filter_piFinset
{n : ℕ}
{α : Fin (n + 1) → Type u_1}
{p : Fin (n + 1)}
(S : (i : Fin (n + 1)) → Finset (α i))
(P : ((i : Fin n) → α (p.succAbove i)) → Prop)
[DecidablePred P]
:
(Finset.filter (fun (r : (i : Fin (n + 1)) → α i) => P (p.removeNth r)) (Fintype.piFinset S)).card = (S p).card * (Finset.filter P (Fintype.piFinset (p.removeNth S))).card