uIcc_subset_Icc — Mathlib

English

If a1 and b1 belong to the closed interval [a2, b2], then the unordered interval [[a1, b1]] is contained in [a2, b2].

Русский

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

LaTeX

$$$ a_1 \\in Icc(a_2,b_2) \\land b_1 \\in Icc(a_2,b_2) \\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₂ :=
  Icc_subset_Icc (le_inf ha.1 hb.1) (sup_le ha.2 hb.2)

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