Fin-indexed tuples of finsets #
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)}
:
cons x_zero x_tail ∈ Fintype.piFinset (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 : α (last n)}
{x_init : (i : Fin n) → α i.castSucc}
{s_last : Finset (α (last n))}
{s_init : (i : Fin n) → Finset (α i.castSucc)}
:
snoc x_init x_last ∈ Fintype.piFinset (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]
:
map (Fin.consEquiv α).symm.toEmbedding ({r ∈ Fintype.piFinset S | P (Fin.tail r)}) = S 0 ×ˢ {r ∈ Fintype.piFinset (Fin.tail S) | P r}
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]
:
map (Fin.snocEquiv α).symm.toEmbedding ({r ∈ Fintype.piFinset S | P (Fin.init r)}) = S (Fin.last n) ×ˢ {r ∈ Fintype.piFinset (Fin.init S) | P r}
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]
:
map (Fin.insertNthEquiv α p).symm.toEmbedding ({r ∈ Fintype.piFinset S | P (p.removeNth r)}) = S p ×ˢ {r ∈ Fintype.piFinset (p.removeNth S) | P r}
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]
:
{r ∈ Fintype.piFinset S | P (Fin.tail r)} = map (Fin.consEquiv α).toEmbedding (S 0 ×ˢ {r ∈ Fintype.piFinset (Fin.tail S) | P r})
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]
:
{r ∈ Fintype.piFinset S | P (Fin.init r)} = map (Fin.snocEquiv α).toEmbedding (S (Fin.last n) ×ˢ {r ∈ Fintype.piFinset (Fin.init S) | P r})
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]
:
{r ∈ Fintype.piFinset S | P (p.removeNth r)} = map (Fin.insertNthEquiv α p).toEmbedding (S p ×ˢ {r ∈ Fintype.piFinset (p.removeNth S) | P r})
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]
:
{r ∈ Fintype.piFinset S | P (Fin.init r)}.card = (S (Fin.last n)).card * {r ∈ Fintype.piFinset (Fin.init S) | P r}.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]
:
{r ∈ Fintype.piFinset S | P (p.removeNth r)}.card = (S p).card * {r ∈ Fintype.piFinset (p.removeNth S) | P r}.card