mem_sSup_of_directedOn — Mathlib

English

For a nonempty directed set K of subgroups of G, the membership in sSup K is equivalent to x ∈ s for some s ∈ K.

Русский

Для ненулевой направленной множества K подгрупп в G принадлежность x к sSup K эквивалентна существованию s ∈ K такое, что x ∈ s.

LaTeX

$$$ x \\in sSup\, K \\;\\iff\\; \\exists s \\in K, x \\in s $$$

Lean4

@[to_additive]
theorem mem_sSup_of_directedOn {K : Set (Subgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (· ≤ ·) K) {x : G} :
    x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s := by
  haveI : Nonempty K := Kne.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed hK.directed_val, SetCoe.exists, exists_prop]

Похожие утверждения