Theorems · Theorem · group theory

Subgroup.mem_biSup_of_directedOn

∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {p : ι → Prop} {K : ι → Subgroup G} {i : ι},
  p i →
    DirectedOn (Function.onFun (fun x1 x2 => x1 ≤ x2) K) {i | p i} →
      ∀ {x : G}, x ∈ ⨆ i, ⨆ (_ : p i), K i ↔ ∃ i, p i ∧ x ∈ K i

Defined in

Mathlib.Algebra.Group.Subgroup.Lattice

Cited by

1 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group