Theorems · Theorem · order theory

csSup_image

∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {s : Set β} {f : β → α},
  BddAbove (Set.range fun i => f ↑i) → sSup ∅ ≤ ⨆ i, f ↑i → sSup (f '' s) = ⨆ a ∈ s, f a

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Indexed

Cited by

3 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLattice