Fin-indexed tuples of finsets

theorem Fin.mem_piFinset_iff_zero_tail {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)

theorem Fin.mem_piFinset_iff_last_init {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 (Fin.last n) ∈ s (Fin.last n) ∧ Fin.init f ∈ Fintype.piFinset (Fin.init s)

theorem Fin.mem_piFinset_iff_pivot_removeNth {n : ℕ} {α : Fin (n + 1) → Type u_1} {f : (i : Fin (n + 1)) → α i} {s : (i : Fin (n + 1)) → Finset (α i)} (p : Fin (n + 1)) : f ∈ Fintype.piFinset s ↔ f p ∈ s p ∧ p.removeNth f ∈ Fintype.piFinset (p.removeNth s)

@[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.

@[deprecated Fin.mem_piFinset_iff_last_init]

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 (Fin.last n) ∈ s (Fin.last n) ∧ Fin.init f ∈ Fintype.piFinset (Fin.init s)

Alias of Fin.mem_piFinset_iff_last_init.

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 (fun (r : (i : Fin n) → α i.succ) => P r) (Fintype.piFinset (Fin.tail S))

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 (fun (r : (i : Fin n) → α i.castSucc) => P r) (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 (fun (r : (i : Fin n) → α (p.succAbove i)) => P r) (Fintype.piFinset (p.removeNth S))

theorem Finset.filter_piFinset_eq_map_consEquiv {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) = Finset.map (Fin.consEquiv α).toEmbedding (S 0 ×ˢ Finset.filter (fun (r : (i : Fin n) → α i.succ) => P r) (Fintype.piFinset (Fin.tail S)))

theorem Finset.filter_piFinset_eq_map_snocEquiv {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) = Finset.map (Fin.snocEquiv α).toEmbedding (S (Fin.last n) ×ˢ Finset.filter (fun (r : (i : Fin n) → α i.castSucc) => P r) (Fintype.piFinset (Fin.init S)))

theorem Finset.filter_piFinset_eq_map_insertNthEquiv {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) = Finset.map (Fin.insertNthEquiv α p).toEmbedding (S p ×ˢ Finset.filter (fun (r : (i : Fin n) → α (p.succAbove i)) => P r) (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 (fun (r : (i : Fin n) → α i.succ) => P r) (Fintype.piFinset (Fin.tail S))).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 (fun (r : (i : Fin n) → α i.castSucc) => P r) (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 (fun (r : (i : Fin n) → α (p.succAbove i)) => P r) (Fintype.piFinset (p.removeNth S))).card