Restriction_of_Associative_Operation_is_Associative
Provedassociativityproofwiki
Let (S, ∘) be a semigroup and T ⊆ S be closed under ∘. Then the restriction of ∘ to T is also associative.
Preamble
import Mathlib.Algebra.Group.Basic import Mathlib.Data.Set.Basic
Formal statement
theorem Restriction_of_Associative_Operation_is_Associative {S : Type _} [Semigroup S] (T : Set S) [Nonempty T] (hclosed : ∀ a b : T, (a : S) * (b : S) ∈ T) : ∀ a b c : T, ((a : S) * (b : S)) * (c : S) = (a : S) * ((b : S) * (c : S)) := by sorrySource