nonUnitalSubsemiringClosure_eq_closure

English

The nonunital subsemiring generated by a multiplicative subsemigroup M coincides with the closure of M as a set.

Русский

Подмножество M как множества и как подсемиринг порождает один и тот же замыкание.

LaTeX

$$M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure (M : Set R)$$

Lean4

/-- The `NonUnitalSubsemiring` generated by a multiplicative subsemigroup coincides with the
`NonUnitalSubsemiring.closure` of the subsemigroup itself . -/
theorem nonUnitalSubsemiringClosure_eq_closure :
    M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure (M : Set R) :=
  by
  ext
  refine
        ⟨fun hx => ?_, fun hx =>
          (NonUnitalSubsemiring.mem_closure.mp hx) M.nonUnitalSubsemiringClosure fun s sM => ?_⟩ <;>
      rintro - ⟨H1, rfl⟩ <;>
    rintro - ⟨H2, rfl⟩
  · exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2
  · exact H2 sM

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