Indicator

theorem indicate_isSelfAdjoint {α : Type u_2} {β : Type u_3} [DecidableEq α] [Semiring β] [StarRing β] (s : Finset α) : IsSelfAdjoint (𝟭 s)

@[simp]

theorem NNReal.coe_indicate {α : Type u_2} [DecidableEq α] (s : Finset α) (x : α) : ↑(𝟭 s x) = 𝟭 s x

@[simp]

theorem NNReal.coe_comp_indicate {α : Type u_2} [DecidableEq α] (s : Finset α) : toReal ∘ 𝟭 s = 𝟭 s

@[simp]

theorem Complex.ofReal_indicate {α : Type u_2} [DecidableEq α] (s : Finset α) (x : α) : ↑(𝟭 s x) = 𝟭 s x

@[simp]

theorem Complex.ofReal_comp_indicate {α : Type u_2} [DecidableEq α] (s : Finset α) : ofReal ∘ 𝟭 s = 𝟭 s

Normalised indicator

@[simp]

theorem Complex.ofReal_mu {α : Type u_2} [DecidableEq α] (s : Finset α) (a : α) : ↑(mu s a) = mu s a

@[simp]

theorem Complex.ofReal_comp_mu {α : Type u_2} [DecidableEq α] (s : Finset α) : ofReal ∘ mu s = mu s

@[simp]

theorem RCLike.coe_mu {α : Type u_2} [DecidableEq α] {𝕜 : Type u_5} [RCLike 𝕜] (s : Finset α) (a : α) : ↑(mu s a) = mu s a

@[simp]

theorem RCLike.coe_comp_mu {α : Type u_2} [DecidableEq α] {𝕜 : Type u_5} [RCLike 𝕜] (s : Finset α) : ofReal ∘ mu s = mu s

@[simp]

theorem NNReal.coe_mu {α : Type u_2} [DecidableEq α] (s : Finset α) (x : α) : ↑(mu s x) = mu s x

@[simp]

theorem NNReal.coe_comp_mu {α : Type u_2} [DecidableEq α] (s : Finset α) : toReal ∘ mu s = mu s