Theorems · Theorem · order theory

OrderIso.map_sSup_eq_sSup_symm_preimage

∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (s : Set α),
  f (sSup s) = sSup (⇑f.symm ⁻¹' s)

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

18 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound

Assumes

CompleteLatticeCompleteLattice