English
There is an order isomorphism between the open-closed intervals Ioo(a ∧ b, a) and Ioo(b, a ∨ b), mirroring the diamond isomorphism for closed intervals.
Русский
Существует порядковый изоморфизм между интервалами Ioo(a ∧ b, a) и Ioo(b, a ∨ b), аналогичный diamond-изоморфизму для замкнутых интервалов.
LaTeX
$$$\text{InfIooOrderIsoIooSup}(a,b): Ioo(a\wedge b,a) \simeq_o Ioo(b,a\vee b).$$$
Lean4
/-- The diamond isomorphism between the intervals `]a ⊓ b, a[` and `}b, a ⊔ b[`. -/
@[simps]
def infIooOrderIsoIooSup (a b : α) : Ioo (a ⊓ b) a ≃o Ioo b (a ⊔ b)
where
toFun
c :=
⟨c ⊔ b,
le_sup_right.trans_lt <| sup_strictMonoOn_Icc_inf (left_mem_Icc.2 inf_le_left) (Ioo_subset_Icc_self c.2) c.2.1,
sup_strictMonoOn_Icc_inf (Ioo_subset_Icc_self c.2) (right_mem_Icc.2 inf_le_left) c.2.2⟩
invFun
c :=
⟨a ⊓ c, inf_strictMonoOn_Icc_sup (left_mem_Icc.2 le_sup_right) (Ioo_subset_Icc_self c.2) c.2.1,
inf_le_left.trans_lt' <| inf_strictMonoOn_Icc_sup (Ioo_subset_Icc_self c.2) (right_mem_Icc.2 le_sup_right) c.2.2⟩
left_inv
c :=
Subtype.ext <| by
dsimp
rw [sup_comm, ← inf_sup_assoc_of_le _ c.prop.2.le, sup_eq_right.2 c.prop.1.le]
right_inv
c :=
Subtype.ext <| by
dsimp
rw [inf_comm, inf_sup_assoc_of_le _ c.prop.1.le, inf_eq_left.2 c.prop.2.le]
map_rel_iff' :=
@fun c d =>
@OrderIso.le_iff_le _ _ _ _ (infIccOrderIsoIccSup _ _) ⟨c.1, Ioo_subset_Icc_self c.2⟩
⟨d.1, Ioo_subset_Icc_self d.2⟩
-- See note [lower instance priority]
