infIccOrderIsoIccSup — Mathlib

English

There is an order isomorphism between the intervals [a ∧ b, a] and [b, a ∨ b], realized by sending x to x ∨ b with the inverse x ↦ a ∧ x.

Русский

Существование порядкового изomорфизма между интервалами [a ∧ b, a] и [b, a ∨ b], заданного переходом x ↦ x ∨ b и обратного перехода.

LaTeX

$$$\operatorname{InfIccOrderIsoIccSup}(a,b): \;\mathrm{Set.Icc}(a\wedge b,a) \simeq_o \mathrm{Set.Icc}(b,a\vee b).$$$

Lean4

/-- The diamond isomorphism between the intervals `[a ⊓ b, a]` and `[b, a ⊔ b]` -/
@[simps]
def infIccOrderIsoIccSup (a b : α) : Set.Icc (a ⊓ b) a ≃o Set.Icc b (a ⊔ b)
    where
  toFun x := ⟨x ⊔ b, ⟨le_sup_right, sup_le_sup_right x.prop.2 b⟩⟩
  invFun x := ⟨a ⊓ x, ⟨inf_le_inf_left a x.prop.1, inf_le_left⟩⟩
  left_inv
    x :=
    Subtype.ext
      (by
        change a ⊓ (↑x ⊔ b) = ↑x
        rw [sup_comm, ← inf_sup_assoc_of_le _ x.prop.2, sup_eq_right.2 x.prop.1])
  right_inv
    x :=
    Subtype.ext
      (by
        change a ⊓ ↑x ⊔ b = ↑x
        rw [inf_comm, inf_sup_assoc_of_le _ x.prop.1, inf_eq_left.2 x.prop.2])
  map_rel_iff'
    {x y} := by
    simp only [Subtype.mk_le_mk, Equiv.coe_fn_mk]
    rw [← Subtype.coe_le_coe]
    refine ⟨fun h => ?_, fun h => sup_le_sup_right h _⟩
    rw [← sup_eq_right.2 x.prop.1, inf_sup_assoc_of_le _ x.prop.2, sup_comm, ← sup_eq_right.2 y.prop.1,
      inf_sup_assoc_of_le _ y.prop.2, sup_comm b]
    exact inf_le_inf_left _ h

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