noncomputable def Set.indicatorOne {α : Type u_1} {R : Type u_2} [One R] [Zero R] (A : Set α) : α → R

A polymorphic indicator function 𝟙_A which is 1 on A and 0 outside.

Equations

• A.indicatorOne = A.indicator fun (x : α) => 1

def Set.«term𝟙__» : Lean.ParserDescr

Equations

• Set.«term𝟙__» = Lean.ParserDescr.node `Set.«term𝟙__» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝟙_") (Lean.ParserDescr.cat `term 1024))