Theorems · Theorem · order theory

LeftOrdContinuous.map_csSup

∀ {α : Type u} {β : Type v} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  {f : α → β}, LeftOrdContinuous f → ∀ {s : Set α}, s.Nonempty → BddAbove s → f (sSup s) = sSup (f '' s)

Defined in

Mathlib.Order.OrdContinuous

Cited by

2 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

ConditionallyCompleteLatticeConditionallyCompleteLattice