coe_set_eq_one — Mathlib

English

A subgroup equals the trivial subgroup if and only if its underlying set equals the singleton {1}.

Русский

Подгруппа равна тривиальной тогда и только тогда, когда её множество равно единичному множеству {1}.

LaTeX

$$(s : Set G) = 1 \iff s = ⊥$$

Lean4

@[norm_cast, to_additive]
theorem coe_set_eq_one [Group G] {s : Subgroup G} : (s : Set G) = 1 ↔ s = ⊥ :=
  (SetLike.ext'_iff.trans (by rfl)).symm

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