Documentation

Mathlib.Data.Fin.Tuple.Finset

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)} :
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)} :
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)} :

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)} :

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 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