uIcc_subset_uIcc — Mathlib

English

Let α be a lattice with a locally finite order. If a1 and b1 lie in the interval between a2 and b2, then the interval between a1 and b1 is contained in the interval between a2 and b2.

Русский

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

LaTeX

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

Lean4

theorem uIcc_subset_uIcc (h₁ : a₁ ∈ [[a₂, b₂]]) (h₂ : b₁ ∈ [[a₂, b₂]]) : [[a₁, b₁]] ⊆ [[a₂, b₂]] :=
  by
  rw [mem_uIcc] at h₁ h₂
  exact Icc_subset_Icc (_root_.le_inf h₁.1 h₂.1) (_root_.sup_le h₁.2 h₂.2)

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