mulIndicator_const — Mathlib

English

For h: EventuallyConst s l, for every c, EventuallyConst (s.mulIndicator (fun _ ↦ c)) l.

Русский

Для любого c, если s константен вдоль l, то индикаторная функция mulIndicator константен вдоль l.

LaTeX

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

Lean4

@[to_additive]
theorem mulIndicator_const (h : EventuallyConst s l) (c : β) : EventuallyConst (s.mulIndicator fun _ ↦ c) l := by
  classical exact h.comp (if · then c else 1)

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