eqOn_mulIndicator' — Mathlib

English

EqOn (mulIndicator s f) 1 on the complement sᶜ; i.e., on sᶜ the indicator is equal to 1.

Русский

EqOn (mulIndicator s f) 1 на комплементе s; то есть на sᶜ индикатор равен 1.

LaTeX

$$$\\mathrm{EqOn}(\\mathrm{mulIndicator}(s,f), 1, s^{\\complement})$$$

Lean4

/-- See `Set.eqOn_mulIndicator` for the version with `s`. -/
@[to_additive /-- See `Set.eqOn_indicator` for the version with `s`. -/
    ]
theorem eqOn_mulIndicator' : EqOn (mulIndicator s f) 1 sᶜ := fun _ hx => mulIndicator_of_notMem hx f

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