theorem Set.indicator_one_inter_apply {α : Type u_2} {M₀ : Type u_4} [MonoidWithZero M₀] (s t : Set α) (x : α) : (s ∩ t).indicator (fun (x : α) => 1) x = s.indicator (fun (x : α) => 1) x * t.indicator (fun (x : α) => 1) x

theorem Set.indicator_one_inter {α : Type u_2} {M₀ : Type u_4} [MonoidWithZero M₀] (s t : Set α) : ((s ∩ t).indicator fun (x : α) => 1) = (s.indicator fun (x : α) => 1) * t.indicator fun (x : α) => 1

theorem Set.map_indicator_one {F : Type u_1} {α : Type u_2} {M₀ : Type u_4} {N₀ : Type u_5} [MonoidWithZero M₀] [MonoidWithZero N₀] [FunLike F M₀ N₀] [MonoidWithZeroHomClass F M₀ N₀] (f : F) (s : Set α) (x : α) : f (s.indicator (fun (x : α) => 1) x) = s.indicator (fun (x : α) => 1) x

@[simp]

theorem Set.indicator_one_image {α : Type u_2} {β : Type u_3} (M₀ : Type u_4) [MonoidWithZero M₀] (e : α ≃ β) (s : Set α) (b : β) : (⇑e '' s).indicator (fun (x : β) => 1) b = s.indicator (fun (x : α) => 1) (e.symm b)

@[simp]

theorem Set.indicator_one_apply_eq_zero {α : Type u_2} {M₀ : Type u_4} [MonoidWithZero M₀] {s : Set α} [Nontrivial M₀] {a : α} : s.indicator (fun (x : α) => 1) a = 0 ↔ ¬a ∈ s

theorem Set.indicator_one_apply_ne_zero {α : Type u_2} {M₀ : Type u_4} [MonoidWithZero M₀] {s : Set α} [Nontrivial M₀] {a : α} : s.indicator (fun (x : α) => 1) a ≠ 0 ↔ a ∈ s

@[simp]

theorem Set.indicator_one_eq_zero {α : Type u_2} {M₀ : Type u_4} [MonoidWithZero M₀] {s : Set α} [Nontrivial M₀] : (s.indicator fun (x : α) => 1) = 0 ↔ s = ∅

theorem Set.indicator_one_ne_zero {α : Type u_2} {M₀ : Type u_4} [MonoidWithZero M₀] {s : Set α} [Nontrivial M₀] : (s.indicator fun (x : α) => 1) ≠ 0 ↔ s.Nonempty

@[simp]

theorem Set.support_indicator_one {α : Type u_2} (M₀ : Type u_4) [MonoidWithZero M₀] {s : Set α} [Nontrivial M₀] : Function.support (s.indicator fun (x : α) => 1) = s