mulIndicator_const_iff_of_ne — Mathlib

English

For hc : c ≠ 1, we have equivalence between EventuallyConst (s.mulIndicator (fun x ↦ c)) l and EventuallyConst s l.

Русский

Для hc : c ≠ 1, имеем эквивалентность между EventuallyConst (s.mulIndicator (fun x ↦ c)) l и EventuallyConst s l.

LaTeX

$$$\mathrm{hc}: c \neq 1 \Rightarrow \mathrm{EventuallyConst} (s.\text{mulIndicator}(\lambda x. c)) l \iff \mathrm{EventuallyConst} s l$$$

Lean4

@[to_additive]
theorem mulIndicator_const_iff_of_ne (hc : c ≠ 1) :
    EventuallyConst (s.mulIndicator fun _ ↦ c) l ↔ EventuallyConst s l :=
  ⟨(of_mulIndicator_const · hc), (mulIndicator_const · c)⟩

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