noncomputable def Set.charfun {α : Type u_1} (a : Set α) : α → Nat

Equations

• a.charfun x = if x ∈ a then 1 else 0

@[simp]

theorem Set.charfun_one_iff {α : Type u_1} {a : Set α} {x : α} : a.charfun x = 1 ↔ x ∈ a

@[simp]

theorem Set.charfun_zero_iff {α : Type u_1} {a : Set α} {x : α} : a.charfun x = 0 ↔ ¬x ∈ a

theorem Set.charfun_zero_or_one {α : Type u_1} (a : Set α) (x : α) : a.charfun x = 0 ∨ a.charfun x = 1

@[simp]

theorem Set.charfun_empty {α : Type u_1} : ∅.charfun = fun (x : α) => 0

@[simp]

theorem Set.charfun_univ {α : Type u_1} : Set.univ.charfun = fun (x : α) => 1

@[simp]

theorem Set.charfun_inter {α : Type u_1} {a b : Set α} : (a ∩ b).charfun = fun (x : α) => a.charfun x * b.charfun x

theorem Set.charfun_union_inter {α : Type u_1} {a b : Set α} {x : α} : (a ∩ b).charfun x + (a ∪ b).charfun x = a.charfun x + b.charfun x

theorem Set.charfun_union {α : Type u_1} {a b : Set α} : (a ∪ b).charfun = fun (x : α) => a.charfun x + b.charfun x - (a ∩ b).charfun x

theorem Set.charfun_inj {α : Type u_1} : Function.Injective Set.charfun

theorem Set.charfun_compl {α : Type u_1} {a : Set α} : aᶜ.charfun = fun (x : α) => 1 - a.charfun x