uIcc_subset_Icc — Mathlib

English

Let α be a lattice with a locally finite order. If a1 and b1 lie in the closed interval Icc(a2, b2), then the Finset interval [[a1, b1]] is contained in Icc(a2, b2).

Русский

Пусть α — решётка с локально конечным порядком. Если a1 и b1 принадлежат замкнутому интервалу Icc(a2, b2), тогда [[a1, b1]] ⊆ Icc(a2, b2).

LaTeX

$$$\bigl(a_1 \in Icc(a_2, b_2) \land b_1 \in Icc(a_2, b_2)\bigr) \Rightarrow [[a_1, b_1]] \subseteq Icc(a_2, b_2)$$$

Lean4

theorem uIcc_subset_Icc (ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂) : [[a₁, b₁]] ⊆ Icc a₂ b₂ :=
  by
  rw [mem_Icc] at ha hb
  exact Icc_subset_Icc (_root_.le_inf ha.1 hb.1) (_root_.sup_le ha.2 hb.2)

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