mem_of_mulIndicator_ne_one — Mathlib

English

If mulIndicator s f a ≠ 1, then a ∈ s.

Русский

Если mulIndicator s f a ≠ 1, значит a ∈ s.

LaTeX

$$$\\mathrm{mulIndicator}(s,f)\\ a \\neq 1 \\Rightarrow a \\in s$$$

Lean4

/-- If a multiplicative indicator function is not equal to `1` at a point, then that point is in the
set. -/
@[to_additive /-- If an additive indicator function is not equal to `0` at a point, then that point is in the set.
    -/
    ]
theorem mem_of_mulIndicator_ne_one (h : mulIndicator s f a ≠ 1) : a ∈ s :=
  not_imp_comm.1 (fun hn => mulIndicator_of_notMem hn f) h

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