English
For U ⊆ α, s ⊆ M and a ∈ M, under decidability assumptions the preimage of s by a constant-indicator equals a union of conditional components depending on membership of a and 1 in s.
Русский
Для U ⊆ α, s ⊆ M и a ∈ M, предобраз s под константным индикатором разлагается на объединение частей в зависимости от принадлежности a и 1 s.
LaTeX
$$$(U.mulIndicator (\\lambda _ => a))^{-1} s = (if a \\in s then U else \\emptyset) \\cup (if (1 : M) \\in s then U^c else \\emptyset)$$$
Lean4
@[to_additive]
theorem mulIndicator_const_preimage_eq_union (U : Set α) (s : Set M) (a : M) [Decidable (a ∈ s)]
[Decidable ((1 : M) ∈ s)] :
(U.mulIndicator fun _ => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if (1 : M) ∈ s then Uᶜ else ∅ :=
by
rw [mulIndicator_preimage, Pi.one_def, Set.preimage_const, preimage_const]
split_ifs <;> simp [← compl_eq_univ_diff]
