mem_iff_boolIndicator

Mathlib.Data.Set.BoolIndicator

URI: https://scilib.ai/kg/mathlib#Set.mem_iff_boolIndicator

English

Let χ_s be the indicator of s. Then x ∈ s iff χ_s(x) = true.

Русский

Пусть χ_s — индикатор множества s. Тогда x ∈ s эквивалентно χ_s(x) = true.

LaTeX

$$$ x \\in s \\iff s.boolIndicator(x) = true $$$

Lean4

theorem mem_iff_boolIndicator (x : α) : x ∈ s ↔ s.boolIndicator x = true :=
  by
  unfold boolIndicator
  split_ifs with h <;> simp [h]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru