notMem_iff_boolIndicator

Mathlib.Data.Set.BoolIndicator

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

English

Let s ⊆ α. Then for every x ∈ α, x ∉ s if and only if the indicator of x in s is false.

Русский

Пусть s ⊆ α. Тогда для каждого x ∈ α выполняется x ∉ s ⇔ I_s(x) = ложь.

LaTeX

$$$x \\notin s \\iff I_s(x) = \\mathrm{false}$$$

Lean4

theorem notMem_iff_boolIndicator (x : α) : x ∉ s ↔ s.boolIndicator x = false :=
  by
  unfold boolIndicator
  split_ifs with h <;> simp [h]

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

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

Разделы

Аффилиация

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