coe_eq_one

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.coe_eq_one

English

The equality of the set corresponding to s with 1 is equivalent to s = 1.

Русский

Равенство множества, соответствующего s, с единицей, эквивалентно тому, что s равно единице.

LaTeX

$$$(s : Set α) = 1 \iff s = 1$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_eq_one : (s : Set α) = 1 ↔ s = 1 :=
  coe_eq_singleton

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru