noncomputable def Finset.pi' {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (t : (i : ι) → Finset (α i)) (ht : ∀ i ∉ s, (↑(t i)).Subsingleton) : Finset ((i : ι) → α i)

Equations

• One or more equations did not get rendered due to their size.

theorem Finset.pi'_of_forall_singleton {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} [DecidableEq ι] (x : (i : ι) → i ∉ s → α i) (ht : ∀ (i : ι) (hi : i ∉ s), t i = {x i hi}) : s.pi' t ⋯ = map { toFun := fun (f : (a : ι) → a ∈ s → α a) (i : ι) => if hi : i ∈ s then f i hi else x i hi, inj' := ⋯ } (s.pi t)

@[simp]

theorem Finset.mem_pi' {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} {x : (i : ι) → α i} (ht : ∀ i ∉ s, (↑(t i)).Subsingleton) : x ∈ s.pi' t ht ↔ ∀ (i : ι), x i ∈ t i

@[simp]

theorem Finset.coe_pi' {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} (ht : ∀ i ∉ s, (↑(t i)).Subsingleton) : ↑(s.pi' t ht) = Set.univ.pi fun (i : ι) => ↑(t i)