boolIndicator — Mathlib

English

Define the indicator function χ_s: α → Bool by χ_s(x) = true if x ∈ s and χ_s(x) = false otherwise.

Русский

Определим индикаторную функцию χ_s: α → Bool так, чтобы χ_s(x) = true, если x ∈ s, и χ_s(x) = false в противном случае.

LaTeX

$$$ \\text{boolIndicator}_s(x) = \\begin{cases} \\text{true}, & x \\in s \\\\ \\text{false}, & x \\notin s \\end{cases}$$$

Lean4

/-- `boolIndicator` maps `x` to `true` if `x ∈ s`, else to `false` -/
noncomputable def boolIndicator (x : α) :=
  @ite _ (x ∈ s) (Classical.propDecidable _) true false

Похожие утверждения