theorem indicator_one_inf_apply {ι : Type u_1} {α : Type u_2} {M₀ : Type u_3} [CommMonoidWithZero M₀] [DecidableEq α] [Fintype α] (s : Finset ι) (t : ι → Finset α) (x : α) : (↑(s.inf t)).indicator (fun (x : α) => 1) x = ∏ i ∈ s, (↑(t i)).indicator (fun (x : α) => 1) x

theorem indicator_one_inf {ι : Type u_1} {α : Type u_2} {M₀ : Type u_3} [CommMonoidWithZero M₀] [DecidableEq α] [Fintype α] (s : Finset ι) (t : ι → Finset α) : ((↑(s.inf t)).indicator fun (x : α) => 1) = ∏ i ∈ s, (↑(t i)).indicator fun (x : α) => 1