Union_of_Subgroups
Provedproofwikiset-unionsubgroupsunion-of-subgroups
Let G be a group. Let H, K be subgroups of G. Let neither H ⊆ K nor K ⊆ H. Then H ∪ K is not a subgroup of G.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Union_of_Subgroups {G : Type _} [Group G] (H K : Subgroup G) (hHK : ¬(H ≤ K)) (hKH : ¬(K ≤ H)) : ¬∃ (L : Subgroup G), ∀ g : G, g ∈ L ↔ (g ∈ H ∨ g ∈ K) := by sorrySource