Ico_subset_Ico_iff — Mathlib

English

For a1 < b1, the half-open interval Ico(a1, b1) is contained in Ico(a2, b2) exactly when a2 ≤ a1 and b1 ≤ b2.

Русский

Для a1 < b1 полузакрытый интервал Ico(a1, b1) содержится в Ico(a2, b2) тогда и только тогда a2 ≤ a1 и b1 ≤ b2.

LaTeX

$$$ a_1 < b_1 \Rightarrow \left( (a_1, b_1) \subseteq (a_2, b_2) \iff a_2 \le a_1 \land b_1 \le b_2 \right)$$$

Lean4

theorem Ico_subset_Ico_iff (h₁ : a₁ < b₁) : Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
  ⟨fun h =>
    have : a₂ ≤ a₁ ∧ a₁ < b₂ := h ⟨le_rfl, h₁⟩
    ⟨this.1, le_of_not_gt fun h' => lt_irrefl b₂ (h ⟨this.2.le, h'⟩).2⟩,
    fun ⟨h₁, h₂⟩ => Ico_subset_Ico h₁ h₂⟩

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