Theorems · Theorem · order theory

IsCompactlyGenerated.BooleanGenerators.sSup_le_sSup_iff_of_atoms

∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α} [IsCompactlyGenerated α],
  IsCompactlyGenerated.BooleanGenerators S → ∀ (X Y : Set α), X ⊆ S → Y ⊆ S → (sSup X ≤ sSup Y ↔ X ⊆ Y)

Defined in

Mathlib.Order.BooleanGenerators

Cited by

0 results in Mathlib

Foundations

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

Assumes

CompleteLatticeIsCompactlyGenerated