English
The indicator of a cylinder, with a constant value, depends only on the coordinates in the index set I.
Русский
Индикатор цилиндра, взятый на константу, зависит только от координат в множестве индексов I.
LaTeX
$$$ \\text{DependsOn}((\\mathrm{cylinder}(I,S)).\\mathrm{indicator}(\\lambda \\_ . c)), I $,$$
Lean4
/-- The indicator of a cylinder only depends on the variables whose the cylinder depends on. -/
theorem dependsOn_cylinder_indicator_const {M : Type*} [Zero M] {I : Finset ι} (S : Set (Π i : I, α i)) (c : M) :
DependsOn ((cylinder I S).indicator (fun _ ↦ c)) I := fun x y hxy ↦
Set.indicator_const_eq_indicator_const (by simp [Finset.restrict_def, hxy])