of_mulIndicator_const — Mathlib

English

If h: EventuallyConst (s.mulIndicator (fun _ ↦ c)) l and c ≠ 1, then EventuallyConst s l.

Русский

Если константная индикаторная функция по множителю s на l не равна 1, то s константен вдоль l.

LaTeX

$$$\mathrm{EventuallyConst}(s.\text{mulIndicator}(\lambda _. c), l) \land c \neq 1 \Rightarrow \mathrm{EventuallyConst}(s, l)$$$

Lean4

@[to_additive]
theorem of_mulIndicator_const (h : EventuallyConst (s.mulIndicator fun _ ↦ c) l) (hc : c ≠ 1) : EventuallyConst s l :=
  by simpa [Function.comp_def, hc, imp_false] using h.comp (· = c)

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