Ioo_subset_Ioo_right — Mathlib

English

Let (α, ≤) be a preorder with a locally finite order. If b1 ≤ b2, then the open interval Ioo(a, b1) is contained in Ioo(a, b2).

Русский

Пусть (α, ≤) — предыдакорядок с локально конечным порядком. Тогда при b1 ≤ b2 выполняется включение Ioo(a, b1) ⊆ Ioo(a, b2).

LaTeX

$$$ (b_1 \le b_2) \Rightarrow Ioo(a,b_1) \subseteq Ioo(a,b_2) $$$

Lean4

theorem Ioo_subset_Ioo_right (h : b₁ ≤ b₂) : Ioo a b₁ ⊆ Ioo a b₂ :=
  Ioo_subset_Ioo le_rfl h

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