Mathlib Map

Theorems · Definition · order theory

infIccOrderIsoIccSup

{α : Type u_1} → [inst : Lattice α] → [IsModularLattice α] → (a b : α) → ↑(Set.Icc (a ⊓ b) a) ≃o ↑(Set.Icc b (a ⊔ b))

The diamond isomorphism between the closed intervals [a ⊓ b, a] and [b, a ⊔ b]

Defined in
Mathlib.Order.ModularLattice
Cited by
6 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext, Quot.sound
Assumes
LatticeIsModularLattice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsCompl.IicOrderIsoIci · cited by 2IsCompl.IicOrderIsoIciinfIccOrderIsoIccSup' · cited by 2infIccOrderIsoIccSup'infIccOrderIsoIccSup.congr_simp · cited by 0infIccOrderIsoIccSup.cong…infIccOrderIsoIccSup'_symm_apply_coe · cited by 0infIccOrderIsoIccSup'_sym…infIccOrderIsoIccSup_apply_coe · cited by 0infIccOrderIsoIccSup_appl…infIccOrderIsoIccSup_symm_apply_coe · cited by 0infIccOrderIsoIccSup_symm…sup_strictMonoOn_Icc_inf · cited by 0sup_strictMonoOn_Icc_infinf_strictMonoOn_Icc_sup · cited by 0inf_strictMonoOn_Icc_supSet · cited by 53352SetSet.Elem · cited by 7166Set.ElemSet.Icc · cited by 1702Set.IccLattice · cited by 916LatticeOrderIso · cited by 874OrderIsoIsModularLattice · cited by 86IsModularLatticeinfIccOrderIsoIccSupCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • Set.Elemstatement and proof · cited by 7,166
  • Set.Iccstatement and proof · cited by 1,702
  • Latticestatement and proof · cited by 916
  • OrderIsostatement · cited by 874
  • IsModularLatticestatement and proof · cited by 86

Cited by8

Results whose statement or proof uses this declaration.