mulIndicator_diff' — Mathlib

English

A variant of the indicator difference identity, expressing mulIndicator (t \\ s) f in terms of mulIndicator t f and mulIndicator s f.

Русский

Вариант тождества разности индикаторов через mulIndicator t f и mulIndicator s f.

LaTeX

$$$$ \\forall s,t:\\ Set\\alpha, s\\subseteq t, \\forall f:\\alpha \\to G,\\ mulIndicator(t \\setminus s) f = mulIndicator t f ÷ mulIndicator s f $$$$

Lean4

@[to_additive indicator_diff]
theorem mulIndicator_diff' (h : s ⊆ t) (f : α → G) : mulIndicator (t \ s) f = mulIndicator t f / mulIndicator s f := by
  rw [mulIndicator_diff h, div_eq_mul_inv]

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