Theorems · Definition · order theory

GaloisCoinsertion.liftLattice

{α : Type u} →
  {β : Type v} →
    {l : α → β} → {u : β → α} → [inst : PartialOrder β] → [inst_1 : Lattice α] → GaloisCoinsertion u l → Lattice β

Lift the suprema and infima along a Galois coinsertion

Defined in

Mathlib.Order.GaloisConnection.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

PartialOrderLattice