Theorems · Theorem · order theory

LowerSet.compl_map

∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (s : LowerSet α),
  ((LowerSet.map f) s).compl = (UpperSet.map f) s.compl

Defined in

Mathlib.Order.UpperLower.CompleteLattice

Cited by

0 results in Mathlib

Foundations

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

Assumes

PreorderPreorder