dependsOn_cylinder_indicator_const

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])

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