mulIndicator_apply_eq_self — Mathlib

English

The equality mulIndicator s f a = f a holds if and only if a ∉ s implies f a = 1.

Русский

Равенство mulIndicator s f a = f a имеет место тогда и только тогда, когда если a ∉ s, то f a = 1.

LaTeX

$$mulIndicator s f a = f a ↔ a ∉ s → f a = 1$$

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_apply_eq_self : s.mulIndicator f a = f a ↔ a ∉ s → f a = 1 :=
  letI := Classical.dec (a ∈ s)
  ite_eq_left_iff.trans (by rw [@eq_comm _ (f a)])

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