@[simp]

theorem ENNReal.ofReal_indicator_one {α : Type u_1} (s : Set α) (a : α) : ENNReal.ofReal (s.indicator 1 a) = s.indicator 1 a

@[simp]

theorem ENNReal.tOReal_indicator_one {α : Type u_1} (s : Set α) (a : α) : (s.indicator 1 a).toReal = s.indicator 1 a