uIcc_subset_uIcc_iff_le' — Mathlib

English

If a1 ∈ Icc(a2,b2) and b1 ∈ Icc(a2,b2) then [[a1,b1]] ⊆ Icc(a2,b2).

Русский

Если a1 ∈ Icc(a2,b2) и 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_uIcc_iff_le' : [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂ :=
  Icc_subset_Icc_iff inf_le_sup

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