mulIndicator_apply_ne_one — Mathlib

English

For any a, mulIndicator s f a ≠ 1 if and only if a ∈ s ∩ mulSupport f.

Русский

Для любого a выполняется mulIndicator s f a ≠ 1 тогда и только тогда, когда a ∈ s ∩ mulSupport f.

LaTeX

$$$\\mathrm{mulIndicator}(s,f)\\ a \\neq 1 \\iff a \\in s \\cap \\mathrm{mulSupport}(f)$$$

Lean4

@[to_additive]
theorem mulIndicator_apply_ne_one {a : α} : s.mulIndicator f a ≠ 1 ↔ a ∈ s ∩ mulSupport f := by
  simp only [Ne, mulIndicator_apply_eq_one, Classical.not_imp, mem_inter_iff, mem_mulSupport]

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