mulIndicator_preimage — Mathlib

English

For any S ⊆ α, f: α → M, and B ⊆ M, the preimage of B under the indicator s.mulIndicator f is given by a standard piecewise expression.

Русский

Для любого S ⊆ α, функции f: α → M и подмножества B ⊆ M, предобраз B под индикатором S.mulIndicator f задаётся обычным подпротивоположным выражением.

LaTeX

$$$(s.mulIndicator f)^{-1} B = s.ite (f^{-1} B) (1^{-1} B)$$$

Lean4

@[to_additive]
theorem mulIndicator_preimage (s : Set α) (f : α → M) (B : Set M) :
    mulIndicator s f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B) :=
  letI := Classical.decPred (· ∈ s)
  piecewise_preimage s f 1 B

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