inter_indicator_one — Mathlib

English

For any f,g: ι → M₀ and sets s,t ⊆ ι, the indicator of the intersection equals the product of indicators: (s ∩ t).indicator 1 = s.indicator 1 · t.indicator 1.

Русский

Для любых f,g: ι → M₀ и множеств s,t ⊆ ι индикатор пересечения равен произведению индикаторов: (s ∩ t).indicator 1 = s.indicator 1 · t.indicator 1.

LaTeX

$$$ (s \cap t).indicator 1 = (s.indicator 1) \cdot (t.indicator 1). $$$

Lean4

theorem inter_indicator_one : (s ∩ t).indicator (1 : ι → M₀) = s.indicator 1 * t.indicator 1 :=
  funext fun _ ↦ by simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]; congr

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