uIcc_subset_uIcc_iff_le — Mathlib

English

For any a1,b1,a2,b2, the unordered interval [[a1,b1]] is contained in [[a2,b2]] if and only if min(a2,b2) ≤ min(a1,b1) and max(a1,b1) ≤ max(a2,b2).

Русский

Для любых a1,b1,a2,b2 неупорядоченный интервал [[a1,b1]] содержится в [[a2,b2]] тогда и только тогда, когда min(a2,b2) ≤ min(a1,b1) и max(a1,b1) ≤ max(a2,b2).

LaTeX

$$$ [[a_1,b_1]] \\subset [[a_2,b_2]] \\iff \\min(a_2,b_2) \\le \\min(a_1,b_1) \\land \\max(a_1,b_1) \\le \\max(a_2,b_2) $$$

Lean4

theorem uIcc_subset_uIcc_iff_le : [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂ :=
  uIcc_subset_uIcc_iff_le'

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