Zulip Chat Archive

Stream: general

Topic: two orphaned lemmas

Scott Morrison (Jul 21 2020 at 12:41):

I'm trying to slice up algebra.big_operators into small files, both because it was getting quite jumbled, and also because every time I look at the output of leanproject import-graph --to X there's an unpleasant knot at algebra.big_operators. :-)

Scott Morrison (Jul 21 2020 at 12:42):

This has mostly gone well, but I've been left with two lemmas, neither of which get used anywhere in mathlib, and neither of which has a natural home anymore.

Scott Morrison (Jul 21 2020 at 12:42):

protected lemma sum_nat_coe_enat (s : finset α) (f : α → ℕ) :
  (∑ x in s, (f x : enat)) = (∑ x  in s, f x : ℕ) :=
begin
  classical,
  induction s using finset.induction with a s has ih h,
  { simp },
  { simp [has, ih] }
end

Scott Morrison (Jul 21 2020 at 12:42):

/-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets
of `s`, and over all subsets of `s` to which one adds `x`. -/
@[to_additive]
lemma prod_powerset_insert [decidable_eq α] [comm_monoid β] {s : finset α} {x : α} (h : x ∉ s) (f : finset α → β) :
  (∏ a in (insert x s).powerset, f a) =
    (∏ a in s.powerset, f a) * (∏ t in s.powerset, f (insert x t)) :=
begin
  rw [powerset_insert, finset.prod_union, finset.prod_image],
  { assume t₁ h₁ t₂ h₂ heq,
    rw [← finset.erase_insert (not_mem_of_mem_powerset_of_not_mem h₁ h),
        ← finset.erase_insert (not_mem_of_mem_powerset_of_not_mem h₂ h), heq] },
  { rw finset.disjoint_iff_ne,
    assume t₁ h₁ t₂ h₂,
    rcases finset.mem_image.1 h₂ with ⟨t₃, h₃, H₃₂⟩,
    rw ← H₃₂,
    exact ne_insert_of_not_mem _ _ (not_mem_of_mem_powerset_of_not_mem h₁ h) }
end