Theorems · Theorem · order theory

Order.IsNormal.preimage_Iic

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

Defined in

Mathlib.Order.IsNormal

Cited by

2 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderConditionallyCompleteLinearOrder