Ioo_subset_Ioo — Mathlib

English

Let α be a preorder. If a₂ ≤ a₁ and b₁ ≤ b₂, then the open interval (a₁, b₁) is contained in (a₂, b₂).

Русский

Пусть α — множество с предикатом упорядоченности. Если a₂ ≤ a₁ и b₁ ≤ b₂, то открытый интервал (a₁, b₁) содержится в интервале (a₂, b₂).

LaTeX

$$$a_2 \le a_1 \land b_1 \le b_2 \Rightarrow Ioo(a_1,b_1) \subseteq Ioo(a_2,b_2)$$$

Lean4

@[gcongr]
theorem Ioo_subset_Ioo (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : Ioo a₁ b₁ ⊆ Ioo a₂ b₂ := fun _ ⟨hx₁, hx₂⟩ =>
  ⟨h₁.trans_lt hx₁, hx₂.trans_le h₂⟩

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