subsemigroup_eq_subgroup_of_ne_top

English

If s ≠ ⊤, then the underlying set of subsemigroup s equals the underlying set of the subgroup s.

Русский

Если s ≠ ⊤, то множество, лежащее в основе подполугруппы s, совпадает с множеством подгруппы s.

LaTeX

$$$s \\neq \\top \\Rightarrow \\text{carrier}(\\text{subsemigroup } s) = \\text{carrier}(\\text{subgroup } s)$$$

Lean4

@[to_additive]
theorem subsemigroup_eq_subgroup_of_ne_top (hs : s ≠ ⊤) : subsemigroup s = (subgroup s : Set M) := by
  simp [subgroup, hs]

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