Theorems · Theorem · order theory

Set.directedOn_sUnion

∀ {α : Type u_1} {r : α → α → Prop} {S : Set (Set α)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) S → (∀ x ∈ S, DirectedOn r x) → DirectedOn r (⋃₀ S)

Defined in

Mathlib.Data.Set.Lattice

Cited by

1 results in Mathlib

Foundations

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