Theorems · Theorem · order theory

RightOrdContinuous.map_csInf

∀ {α : Type u} {β : Type v} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  {f : α → β}, RightOrdContinuous f → ∀ {s : Set α}, s.Nonempty → BddBelow s → f (sInf s) = sInf (f '' s)

Defined in

Mathlib.Order.OrdContinuous

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

ConditionallyCompleteLatticeConditionallyCompleteLattice