Theorems · Theorem · order theory

Order.IsNormal.map_sSup

∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLinearOrder β],
  Order.IsNormal f → ∀ {s : Set α}, s.Nonempty → BddAbove s → f (sSup s) = sSup (f '' s)

Defined in

Mathlib.Order.IsNormal

Cited by

5 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderConditionallyCompleteLinearOrder