English
Let G be a group and {K_i} a directed family of subgroups indexed by ι with a predicate p on ι. For any i with p(i) and any x in G, x lies in the directed bi-supremum iff x is contained in some K_i with p(i).
Русский
Пусть G — группа, и {K_i} — направленная семья подгрупп, индексируемая ι, с предикатом p на ι. Для любого i, удовлетворяющего p(i), и для любого x ∈ G, x принадлежит направленному би-супремуму тогда и только тогда, когда x ∈ K_i для некоторого i с p(i).
LaTeX
$$$ x \\in \\bigvee_{i} \\big( \\bigvee_{h: p(i)} K_i \\big) \\;\\Longleftrightarrow\\; \\exists i, p(i) \\land x \\in K_i $$$
Lean4
@[to_additive]
theorem mem_biSup_of_directedOn {ι} {p : ι → Prop} {K : ι → Subgroup G} {i : ι} (hp : p i)
(hK : DirectedOn ((· ≤ ·) on K) {i | p i}) {x : G} : x ∈ (⨆ i, ⨆ (_h : p i), K i) ↔ ∃ i, p i ∧ x ∈ K i := by
-- Could use the `Submonoid` version, but we limit the imports here
refine ⟨?_, fun ⟨i, hi', hi⟩ ↦ ?_⟩
· suffices x ∈ closure (⋃ i, ⋃ (_ : p i), (K i : Set G)) → ∃ i, p i ∧ x ∈ K i by
simpa only [closure_iUnion, closure_eq (K _)] using this
refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx
· simp
· exact ⟨i, hp, (K i).one_mem⟩
· rintro x y _ _ ⟨i, hip, hi⟩ ⟨j, hjp, hj⟩
rcases hK i hip j hjp with ⟨k, hk, hki, hkj⟩
exact ⟨k, hk, mul_mem (hki hi) (hkj hj)⟩
· rintro _ _ ⟨i, hi', hi⟩
exact ⟨i, hi', inv_mem hi⟩
· apply le_iSup (fun i ↦ ⨆ (_ : p i), K i) i
simp [hi, hi']
