mulIndicator_preimage_of_notMem — Mathlib

English

If 1 is not in t, then mulIndicator s f preimage t equals f preimage t intersect s.

Русский

Если 1 не принадлежит t, тогда mulIndicator s f^{-1}(t) = (f^{-1}(t)) ∩ s.

LaTeX

$$$mulIndicator s f ^{-1} t = f ^{-1} t \\cap s$$$

Lean4

@[to_additive]
theorem mulIndicator_preimage_of_notMem (s : Set α) (f : α → M) {t : Set M} (ht : (1 : M) ∉ t) :
    mulIndicator s f ⁻¹' t = f ⁻¹' t ∩ s := by simp [mulIndicator_preimage, Pi.one_def, Set.preimage_const_of_notMem ht]

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