uIcc_subset_uIcc_iff_le' — Mathlib

English

The inclusion [[a1, b1]] ⊆ [[a2, b2]] holds if and only if min(a2, b2) ≤ min(a1, b1) and max(a1, b1) ≤ max(a2, b2).

Русский

Включение [[a1, b1]] ⊆ [[a2, b2]] эквивалентно тому, что min(a2, b2) ≤ min(a1, b1) и max(a1, b1) ≤ max(a2, b2).

LaTeX

$$$ [[a_1,b_1]] \\subseteq [[a_2,b_2]] \\iff (a_2 \\land b_2) \\le (a_1 \\land b_1) \\land (a_1 \\lor b_1) \\le (a_2 \\lor b_2) $$$

Lean4

theorem uIcc_subset_uIcc_iff_le' : [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂ :=
  Icc_subset_Icc_iff inf_le_sup

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