Theorems · Theorem · order theory

IsModularLattice.exists_inf_eq_and_sup_eq

∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a b c : α} [inst_2 : BoundedOrder α] [ComplementedLattice α],
  a ≤ b → b ≤ c → ∃ b', b ⊓ b' = a ∧ b ⊔ b' = c

Defined in

Mathlib.Order.ModularLattice

Cited by

2 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext

Assumes

LatticeIsModularLatticeBoundedOrderComplementedLattice