to_isUpperModularLattice — Mathlib

English

Further properties of the open-interval diamond isomorphism in a modular lattice.

Русский

Дополнительные свойства diamond-изоморфизма между открытыми интервалами в модульной решётке.

LaTeX

$$$\forall a,b,\text{ the isomorphism respects endpoints and preserves order.}$$$

Lean4

instance (priority := 100) to_isUpperModularLattice : IsUpperModularLattice α :=
  ⟨fun {a b} =>
    by
    simp_rw [covBy_iff_Ioo_eq, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left,
      (infIooOrderIsoIooSup a b).toEquiv.isEmpty_congr]
    exact id⟩

Похожие утверждения