Documentation

Mathlib.Data.Set.BoolIndicator

Indicator function valued in bool #

See also Set.indicator and Set.piecewise.

noncomputable def Set.boolIndicator {α : Type u_1} (s : Set α) (x : α) :

boolIndicator maps x to true if x ∈ s, else to false

Equations
    Instances For
      theorem Set.mem_iff_boolIndicator {α : Type u_1} (s : Set α) (x : α) :
      theorem Set.notMem_iff_boolIndicator {α : Type u_1} (s : Set α) (x : α) :
      xs s.boolIndicator x = false
      @[deprecated Set.notMem_iff_boolIndicator (since := "2025-05-23")]
      theorem Set.not_mem_iff_boolIndicator {α : Type u_1} (s : Set α) (x : α) :
      xs s.boolIndicator x = false

      Alias of Set.notMem_iff_boolIndicator.