Theorems · Theorem · order theory

iSup_inf_of_monotone

∀ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} [inst_1 : Preorder ι] [IsDirectedOrder ι] {f g : ι → α},
  Monotone f → Monotone g → ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i

Defined in

Mathlib.Order.CompleteBooleanAlgebra

Cited by

3 results in Mathlib

Foundations

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

Assumes

Order.FramePreorderIsDirectedOrder