Theorems · Definition · order theory

LowerSet.map

{α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β → LowerSet α ≃o LowerSet β

An order isomorphism of Preorders induces an order isomorphism of their lower sets.

Defined in

Mathlib.Order.UpperLower.CompleteLattice

Cited by

12 results in Mathlib

Foundations

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

Assumes

PreorderPreorder