indicator_one_inj — Mathlib

English

If the indicator functions of 1 on sets s and t are equal, then s = t. More precisely, if indicator_s 1 = indicator_t 1, then s = t.

Русский

Если индикаторы 1 на множествах s и t равны, то s = t.

LaTeX

$$$ \text{If } \operatorname{indicator}_s 1 = \operatorname{indicator}_t 1, \text{ then } s = t. $$$

Lean4

theorem indicator_one_inj (h : indicator s (1 : ι → M₀) = indicator t 1) : s = t := by ext;
  simp_rw [← indicator_eq_one_iff_mem M₀, h]

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