to_isLowerModularLattice — Mathlib

English

A formal construction of the diamond isomorphism between Ioo intervals for modular lattices with IsModularLattice structure.

Русский

Формальная конструкция diamond-изоморфизма между интервалами Ioo для модульных решёток.

LaTeX

$$$\text{InfIooOrderIsoIooSup}(a,b)\text{ is an order isomorphism between } Ioo(a\wedge b,a) \text{ and } Ioo(b,a\vee b).$$$

Lean4

instance (priority := 100) to_isLowerModularLattice : IsLowerModularLattice α :=
  ⟨fun {a b} =>
    by
    simp_rw [covBy_iff_Ioo_eq, sup_comm a, inf_comm a, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left,
      (infIooOrderIsoIooSup b a).symm.toEquiv.isEmpty_congr]
    exact id⟩
    -- See note [lower instance priority]

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