Theorems · Theorem · order theory

JordanHolderLattice.Iso.rel

∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (e : X × X → X × X → Prop),
  (∀ {x : X × X}, e x x) →
    (∀ {x y : X × X}, e x y → e y x) →
      (∀ {x y z : X × X}, e x y → e y z → e x z) →
        (∀ {x y : X}, JordanHolderLattice.IsMaximal x (x ⊔ y) → e (x, x ⊔ y) (x ⊓ y, y)) →
          ∀ {x y : X × X}, JordanHolderLattice.Iso x y → e x y

The equivalence relation on intervals implies any other notions of isomorphism.

Defined in

Mathlib.Order.JordanHolder

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

LatticeJordanHolderLattice