preimage_boolIndicator_false

Mathlib.Data.Set.BoolIndicator

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

English

Let s ⊆ α. Then the preimage of { false } under the indicator is the complement of s.

Русский

Пусть s ⊆ α. Тогда прообраз {false} индикатора равен дополнению множества s.

LaTeX

$$$(I_s)^{-1}(\{\\mathrm{false}\\}) = s^{\\mathrm{c}}$$$

Lean4

theorem preimage_boolIndicator_false : s.boolIndicator ⁻¹' { false } = sᶜ :=
  ext fun x ↦ (s.notMem_iff_boolIndicator x).symm

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

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

Разделы

Аффилиация

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