English
For any subset t of {true,false}, the preimage under the indicator is the union of the parts corresponding to true and false membership in t: s.boolIndicator^{-1}(t) = (if true ∈ t then s else ∅) ∪ (if false ∈ t then sᶜ else ∅).
Русский
Для любого подмножества t ⊆ {true,false} прообраз под индикатором равно объединению соответствующих частей: s.boolIndicator^{-1}(t) = (если true ∈ t, то s, иначе ∅) ∪ (если false ∈ t, то s^c, иначе ∅).
LaTeX
$$$s.boolIndicator^{-1} t = (\\text{if } true \\in t \\text{ then } s \\text{ else } \\emptyset) \\cup (\\text{if } false \\in t \\text{ then } s^{\\mathrm{c}} \\text{ else } \\emptyset)$$$
Lean4
theorem preimage_boolIndicator_eq_union (t : Set Bool) :
s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅ :=
by
ext x
simp only [boolIndicator, mem_preimage]
split_ifs <;> simp [*]
