English
If {K_i} is a directed family of subgroups of G indexed by ι and ι is nonempty, then the membership in the supremum of K_i equals membership in some K_i: x ∈ iSup K ⇔ ∃ i, x ∈ K_i.
Русский
Если {K_i} — направленная семья подгрупп подгрупп G индексируемая ι и ι непусто, то принадлежность xọi верхнему объединению равна принадлежности x некоторому K_i: x ∈ iSup K ⇔ ∃ i, x ∈ K_i.
LaTeX
$$$ x \\in (\\iSup K : Subgroup\, G) \\;\\iff\\; \\exists i, x \\in K_i $$$
Lean4
@[to_additive]
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {K : ι → Subgroup G} (hK : Directed (· ≤ ·) K) {x : G} :
x ∈ (iSup K : Subgroup G) ↔ ∃ i, x ∈ K i :=
by
have : iSup K = ⨆ i : PLift ι, ⨆ (_ : True), K i.down := by simp [iSup_plift_down]
rw [this, mem_biSup_of_directedOn trivial]
· simp
· simp only [setOf_true]
rw [directedOn_onFun_iff, Set.image_univ, ← directedOn_range]
-- `Directed.mono_comp` and much of the Set API requires `Type u` instead of `Sort u`
intro i
simp only [PLift.exists]
intro j
refine (hK i.down j.down).imp ?_
simp
· exact PLift.up hι.some
