Icc_subset_Icc — Mathlib

English

Let α be a preorder. If a₂ ≤ a₁ and b₁ ≤ b₂, then Icc(a₁, b₁) ⊆ Icc(a₂, b₂).

Русский

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

LaTeX

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

Lean4

@[gcongr]
theorem Icc_subset_Icc (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : Icc a₁ b₁ ⊆ Icc a₂ b₂ := fun _ ⟨hx₁, hx₂⟩ =>
  ⟨h₁.trans hx₁, le_trans hx₂ h₂⟩

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