map_mulIndicator — Mathlib

English

A reiteration of the difference identity for mulIndicator, relating t \\ s to the quotients of the full and sub-indicators.

Русский

Повторение тождества разности индикаторов через частное от полного и частичных индикаторов.

LaTeX

$$$$ \\forall s \\subseteq t, \\forall f,\\ mulIndicator(t \\setminus s) f = mulIndicator t f / mulIndicator s f $$$$

Lean4

@[to_additive]
theorem map_mulIndicator {M N : Type*} [MulOneClass M] [MulOneClass N] (f : M →* N) (s : Set α) (g : α → M) (x : α) :
    f (s.mulIndicator g x) = s.mulIndicator (f ∘ g) x := by simp [Set.mulIndicator_comp_of_one]

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