mulIndicator_const_iff — Mathlib

English

For any [One β], EventuallyConst (s.mulIndicator (fun _ ↦ c)) l is equivalent to (c = 1) or EventuallyConst s l.

Русский

Для произвольного элемента c, если β имеет единичный элемент, then EventuallyConst (s.mulIndicator (fun _ ↦ c)) l эквивалентно (c = 1) или EventuallyConst s l.

LaTeX

$$$\mathrm{EventuallyConst}(s.\text{mulIndicator}(\lambda x. c), l) \iff (c = 1 \lor \mathrm{EventuallyConst}(s, l))$$$

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_const_iff : EventuallyConst (s.mulIndicator fun _ ↦ c) l ↔ c = 1 ∨ EventuallyConst s l := by
  rcases eq_or_ne c 1 with rfl | hc <;> simp [mulIndicator_const_iff_of_ne, *]

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