Directed union of subobject

Stream: Is there code for X?

[Chris Hughes]

Do we have an undeprecated version of

@[to_additive]
lemma is_subgroup_Union_of_directed {ι : Type*} [hι : nonempty ι]
  {s : ι → set G} (hs : ∀ i, is_subgroup (s i))
  (directed : ∀ i j, ∃ k, s i ⊆ s k ∧ s j ⊆ s k) :
  is_subgroup (⋃i, s i) :=
{ inv_mem := λ a ha,
    let ⟨i, hi⟩ := set.mem_Union.1 ha in
    set.mem_Union.2 ⟨i, (hs i).inv_mem hi⟩,
  to_is_submonoid := is_submonoid_Union_of_directed (λ i, (hs i).to_is_submonoid) directed }

I need it for subalgebras and I'm curious about the best way to state it.

[Ruben Van de Velde]

Would something like this work?

import group_theory.subgroup

variables {G : Type*} [group G]

def t {ι : Type*} [hι : nonempty ι]
  {s : ι → subgroup G}
  (directed : ∀ i j, ∃ k, (s i : set G) ⊆ s k ∧ (s j : set G) ⊆ s k) : subgroup G :=
{ carrier := ⋃i, s i,
  one_mem' :=
    let ⟨i⟩ := hι in set.mem_Union.2 ⟨i, (s i).one_mem⟩,
  mul_mem' := λ a b ha hb,
    let ⟨i, hi⟩ := set.mem_Union.1 ha in
    let ⟨j, hj⟩ := set.mem_Union.1 hb in
    let ⟨k, hk⟩ := directed i j in
    set.mem_Union.2 ⟨k, (s k).mul_mem (hk.1 hi) (hk.2 hj)⟩,
  inv_mem' := λ a ha,
    let ⟨i, hi⟩ := set.mem_Union.1 ha in
    set.mem_Union.2 ⟨i, (s i).inv_mem hi⟩ }

[Kevin Buzzard]

We have docs#subgroup.mem_supr_of_directed